% Mizar problem: t68_funct_5,funct_5,1428,33 
fof(t68_funct_5,conjecture,(
    ! [A,B,C,D] : 
      ( ( k1_card_1(A) = k1_card_1(B)
        & k1_card_1(C) = k1_card_1(D) )
     => k1_card_1(k1_funct_2(A,C)) = k1_card_1(k1_funct_2(B,D)) ) ),
    inference(mizar_bg_added,[status(thm)],[dt_k1_card_1,dt_k1_funct_2,redefinition_r2_wellord2,reflexivity_r2_wellord2,symmetry_r2_wellord2,t21_card_1,t67_funct_5]),
    [file(funct_5,t68_funct_5)]).

fof(dt_k1_card_1,axiom,(
    ! [A] : v1_card_1(k1_card_1(A)) ),
    file(card_1,k1_card_1),
    []).

fof(dt_k1_funct_2,axiom,(
    $true ),
    file(funct_2,k1_funct_2),
    []).

fof(redefinition_r2_wellord2,axiom,(
    ! [A,B] : 
      ( r2_wellord2(A,B)
    <=> r2_tarski(A,B) ) ),
    file(wellord2,r2_wellord2),
    []).

fof(reflexivity_r2_wellord2,axiom,(
    ! [A,B] : r2_wellord2(A,A) ),
    file(wellord2,r2_wellord2),
    []).

fof(symmetry_r2_wellord2,axiom,(
    ! [A,B] : 
      ( r2_wellord2(A,B)
     => r2_wellord2(B,A) ) ),
    file(wellord2,r2_wellord2),
    []).

fof(t21_card_1,axiom,(
    ! [A,B] : 
      ( r2_wellord2(A,B)
    <=> k1_card_1(A) = k1_card_1(B) ) ),
    file(card_1,t21_card_1),
    []).

fof(t67_funct_5,axiom,(
    ! [A,B,C,D] : 
      ( ( r2_wellord2(A,B)
        & r2_wellord2(C,D) )
     => ( r2_wellord2(k1_funct_2(A,C),k1_funct_2(B,D))
        & k1_card_1(k1_funct_2(A,C)) = k1_card_1(k1_funct_2(B,D)) ) ) ),
    file(funct_5,t67_funct_5),
    []).