% Mizar problem: t4_recdef_2,recdef_2,153,72 
fof(t4_recdef_2,conjecture,(
    ! [A] : 
      ( ? [B,C,D,E] : A = k4_mcart_1(B,C,D,E)
     => A = k4_mcart_1(k4_recdef_2(A),k5_recdef_2(A),k6_recdef_2(A),k7_recdef_2(A)) ) ),
    inference(mizar_bg_added,[status(thm)],[d4_recdef_2,d5_recdef_2,d6_recdef_2,d7_recdef_2,dt_k4_mcart_1,dt_k4_recdef_2,dt_k5_recdef_2,dt_k6_recdef_2,dt_k7_recdef_2]),
    [file(recdef_2,t4_recdef_2)]).

fof(d4_recdef_2,axiom,(
    ! [A] : 
      ( ? [B,C,D,E] : A = k4_mcart_1(B,C,D,E)
     => ! [B] : 
          ( B = k4_recdef_2(A)
        <=> ! [C,D,E,F] : 
              ( A = k4_mcart_1(C,D,E,F)
             => B = C ) ) ) ),
    file(recdef_2,d4_recdef_2),
    []).

fof(d5_recdef_2,axiom,(
    ! [A] : 
      ( ? [B,C,D,E] : A = k4_mcart_1(B,C,D,E)
     => ! [B] : 
          ( B = k5_recdef_2(A)
        <=> ! [C,D,E,F] : 
              ( A = k4_mcart_1(C,D,E,F)
             => B = D ) ) ) ),
    file(recdef_2,d5_recdef_2),
    []).

fof(d6_recdef_2,axiom,(
    ! [A] : 
      ( ? [B,C,D,E] : A = k4_mcart_1(B,C,D,E)
     => ! [B] : 
          ( B = k6_recdef_2(A)
        <=> ! [C,D,E,F] : 
              ( A = k4_mcart_1(C,D,E,F)
             => B = E ) ) ) ),
    file(recdef_2,d6_recdef_2),
    []).

fof(d7_recdef_2,axiom,(
    ! [A] : 
      ( ? [B,C,D,E] : A = k4_mcart_1(B,C,D,E)
     => ! [B] : 
          ( B = k7_recdef_2(A)
        <=> ! [C,D,E,F] : 
              ( A = k4_mcart_1(C,D,E,F)
             => B = F ) ) ) ),
    file(recdef_2,d7_recdef_2),
    []).

fof(dt_k4_mcart_1,axiom,(
    $true ),
    file(mcart_1,k4_mcart_1),
    []).

fof(dt_k4_recdef_2,axiom,(
    $true ),
    file(recdef_2,k4_recdef_2),
    []).

fof(dt_k5_recdef_2,axiom,(
    $true ),
    file(recdef_2,k5_recdef_2),
    []).

fof(dt_k6_recdef_2,axiom,(
    $true ),
    file(recdef_2,k6_recdef_2),
    []).

fof(dt_k7_recdef_2,axiom,(
    $true ),
    file(recdef_2,k7_recdef_2),
    []).