% Mizar problem: t23_absvalue,absvalue,184,54 
fof(t23_absvalue,conjecture,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( ~ r1_xreal_0(k7_xcmplx_0(A,B),0)
           => k8_square_1(k7_xcmplx_0(A,B)) = k6_real_1(k9_square_1(k18_complex1(A)),k9_square_1(k18_complex1(B))) ) ) ) ),
    inference(mizar_bg_added,[status(thm)],[cc1_real_1,cc2_xreal_0,connectedness_r1_xreal_0,d1_absvalue,dt_k16_complex1,dt_k18_complex1,dt_k1_numbers,dt_k4_xcmplx_0,dt_k6_real_1,dt_k7_xcmplx_0,dt_k8_square_1,dt_k9_square_1,dt_m1_subset_1,existence_m1_subset_1,fc1_xreal_0,fc6_xreal_0,involutiveness_k4_xcmplx_0,l21_absvalue,l3_absvalue,projectivity_k16_complex1,projectivity_k18_complex1,rc1_xreal_0,redefinition_k18_complex1,redefinition_k6_real_1,redefinition_k9_square_1,reflexivity_r1_xreal_0,t5_arithm,t99_square_1]),
    [file(absvalue,t23_absvalue)]).

fof(cc1_real_1,axiom,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ( v1_xreal_0(A)
        & v1_xcmplx_0(A) ) ) ),
    file(real_1,cc1_real_1),
    []).

fof(cc2_xreal_0,axiom,(
    ! [A] : 
      ( v1_xreal_0(A)
     => v1_xcmplx_0(A) ) ),
    file(xreal_0,cc2_xreal_0),
    []).

fof(connectedness_r1_xreal_0,axiom,(
    ! [A,B] : 
      ( ( v1_xreal_0(A)
        & v1_xreal_0(B) )
     => ( r1_xreal_0(A,B)
        | r1_xreal_0(B,A) ) ) ),
    file(xreal_0,r1_xreal_0),
    []).

fof(d1_absvalue,axiom,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( ( r1_xreal_0(0,A)
         => k16_complex1(A) = A )
        & ( ~ r1_xreal_0(0,A)
         => k16_complex1(A) = k4_xcmplx_0(A) ) ) ) ),
    file(absvalue,d1_absvalue),
    []).

fof(dt_k16_complex1,axiom,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => v1_xcmplx_0(k16_complex1(A)) ) ),
    file(complex1,k16_complex1),
    []).

fof(dt_k18_complex1,axiom,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => m1_subset_1(k18_complex1(A),k1_numbers) ) ),
    file(complex1,k18_complex1),
    []).

fof(dt_k1_numbers,axiom,(
    $true ),
    file(numbers,k1_numbers),
    []).

fof(dt_k4_xcmplx_0,axiom,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => v1_xcmplx_0(k4_xcmplx_0(A)) ) ),
    file(xcmplx_0,k4_xcmplx_0),
    []).

fof(dt_k6_real_1,axiom,(
    ! [A,B] : 
      ( ( m1_subset_1(A,k1_numbers)
        & m1_subset_1(B,k1_numbers) )
     => m1_subset_1(k6_real_1(A,B),k1_numbers) ) ),
    file(real_1,k6_real_1),
    []).

fof(dt_k7_xcmplx_0,axiom,(
    $true ),
    file(xcmplx_0,k7_xcmplx_0),
    []).

fof(dt_k8_square_1,axiom,(
    ! [A] : 
      ( v1_xreal_0(A)
     => v1_xreal_0(k8_square_1(A)) ) ),
    file(square_1,k8_square_1),
    []).

fof(dt_k9_square_1,axiom,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => m1_subset_1(k9_square_1(A),k1_numbers) ) ),
    file(square_1,k9_square_1),
    []).

fof(dt_m1_subset_1,axiom,(
    $true ),
    file(subset_1,m1_subset_1),
    []).

fof(existence_m1_subset_1,axiom,(
    ! [A] : 
    ? [B] : m1_subset_1(B,A) ),
    file(subset_1,m1_subset_1),
    []).

fof(fc1_xreal_0,axiom,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( v1_xcmplx_0(k4_xcmplx_0(A))
        & v1_xreal_0(k4_xcmplx_0(A)) ) ) ),
    file(xreal_0,fc1_xreal_0),
    []).

fof(fc6_xreal_0,axiom,(
    ! [A,B] : 
      ( ( v1_xreal_0(A)
        & v1_xreal_0(B) )
     => ( v1_xcmplx_0(k7_xcmplx_0(A,B))
        & v1_xreal_0(k7_xcmplx_0(A,B)) ) ) ),
    file(xreal_0,fc6_xreal_0),
    []).

fof(involutiveness_k4_xcmplx_0,axiom,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k4_xcmplx_0(k4_xcmplx_0(A)) = A ) ),
    file(xcmplx_0,k4_xcmplx_0),
    []).

fof(l21_absvalue,axiom,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => k18_complex1(k7_xcmplx_0(A,B)) = k6_real_1(k18_complex1(A),k18_complex1(B)) ) ) ),
    file(absvalue,l21_absvalue),
    []).

fof(l3_absvalue,axiom,(
    ! [A] : 
      ( v1_xreal_0(A)
     => r1_xreal_0(0,k18_complex1(A)) ) ),
    file(absvalue,l3_absvalue),
    []).

fof(projectivity_k16_complex1,axiom,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k16_complex1(k16_complex1(A)) = k16_complex1(A) ) ),
    file(complex1,k16_complex1),
    []).

fof(projectivity_k18_complex1,axiom,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k18_complex1(k18_complex1(A)) = k18_complex1(A) ) ),
    file(complex1,k18_complex1),
    []).

fof(rc1_xreal_0,axiom,(
    ? [A] : 
      ( v1_xcmplx_0(A)
      & v1_xreal_0(A) ) ),
    file(xreal_0,rc1_xreal_0),
    []).

fof(redefinition_k18_complex1,axiom,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k18_complex1(A) = k16_complex1(A) ) ),
    file(complex1,k18_complex1),
    []).

fof(redefinition_k6_real_1,axiom,(
    ! [A,B] : 
      ( ( m1_subset_1(A,k1_numbers)
        & m1_subset_1(B,k1_numbers) )
     => k6_real_1(A,B) = k7_xcmplx_0(A,B) ) ),
    file(real_1,k6_real_1),
    []).

fof(redefinition_k9_square_1,axiom,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => k9_square_1(A) = k8_square_1(A) ) ),
    file(square_1,k9_square_1),
    []).

fof(reflexivity_r1_xreal_0,axiom,(
    ! [A,B] : 
      ( ( v1_xreal_0(A)
        & v1_xreal_0(B) )
     => r1_xreal_0(A,A) ) ),
    file(xreal_0,r1_xreal_0),
    []).

fof(t5_arithm,axiom,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k7_xcmplx_0(0,A) = 0 ) ),
    file(arithm,t5_arithm),
    []).

fof(t99_square_1,axiom,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( ( r1_xreal_0(0,A)
              & r1_xreal_0(0,B) )
           => k8_square_1(k7_xcmplx_0(A,B)) = k7_xcmplx_0(k8_square_1(A),k8_square_1(B)) ) ) ) ),
    file(square_1,t99_square_1),
    []).