% Mizar problem: t1_recdef_2,recdef_2,70,61 
fof(t1_recdef_2,conjecture,(
    ! [A] : 
      ( ? [B,C,D] : A = k3_mcart_1(B,C,D)
     => A = k3_mcart_1(k1_recdef_2(A),k2_recdef_2(A),k3_recdef_2(A)) ) ),
    inference(mizar_bg_added,[status(thm)],[d1_recdef_2,d2_recdef_2,d3_recdef_2,dt_k1_recdef_2,dt_k2_recdef_2,dt_k3_mcart_1,dt_k3_recdef_2]),
    [file(recdef_2,t1_recdef_2)]).

fof(d1_recdef_2,axiom,(
    ! [A] : 
      ( ? [B,C,D] : A = k3_mcart_1(B,C,D)
     => ! [B] : 
          ( B = k1_recdef_2(A)
        <=> ! [C,D,E] : 
              ( A = k3_mcart_1(C,D,E)
             => B = C ) ) ) ),
    file(recdef_2,d1_recdef_2),
    []).

fof(d2_recdef_2,axiom,(
    ! [A] : 
      ( ? [B,C,D] : A = k3_mcart_1(B,C,D)
     => ! [B] : 
          ( B = k2_recdef_2(A)
        <=> ! [C,D,E] : 
              ( A = k3_mcart_1(C,D,E)
             => B = D ) ) ) ),
    file(recdef_2,d2_recdef_2),
    []).

fof(d3_recdef_2,axiom,(
    ! [A] : 
      ( ? [B,C,D] : A = k3_mcart_1(B,C,D)
     => ! [B] : 
          ( B = k3_recdef_2(A)
        <=> ! [C,D,E] : 
              ( A = k3_mcart_1(C,D,E)
             => B = E ) ) ) ),
    file(recdef_2,d3_recdef_2),
    []).

fof(dt_k1_recdef_2,axiom,(
    $true ),
    file(recdef_2,k1_recdef_2),
    []).

fof(dt_k2_recdef_2,axiom,(
    $true ),
    file(recdef_2,k2_recdef_2),
    []).

fof(dt_k3_mcart_1,axiom,(
    $true ),
    file(mcart_1,k3_mcart_1),
    []).

fof(dt_k3_recdef_2,axiom,(
    $true ),
    file(recdef_2,k3_recdef_2),
    []).