% Mizar problem: t11_funcop_1,funcop_1,274,20 
fof(t11_funcop_1,conjecture,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ! [C] : k7_relat_1(k13_funct_3(A,B),C) = k13_funct_3(A,k7_relat_1(B,C)) ) ) ),
    inference(mizar_bg_added,[status(thm)],[dt_k13_funct_3,dt_k1_funcop_1,dt_k7_relat_1,fc4_funct_1,involutiveness_k1_funcop_1,rc1_funct_1,t10_funcop_1,t6_funcop_1,t7_funcop_1]),
    [file(funcop_1,t11_funcop_1)]).

fof(dt_k13_funct_3,axiom,(
    ! [A,B] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_relat_1(B)
        & v1_funct_1(B) )
     => ( v1_relat_1(k13_funct_3(A,B))
        & v1_funct_1(k13_funct_3(A,B)) ) ) ),
    file(funct_3,k13_funct_3),
    []).

fof(dt_k1_funcop_1,axiom,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( v1_relat_1(k1_funcop_1(A))
        & v1_funct_1(k1_funcop_1(A)) ) ) ),
    file(funcop_1,k1_funcop_1),
    []).

fof(dt_k7_relat_1,axiom,(
    ! [A,B] : 
      ( v1_relat_1(A)
     => v1_relat_1(k7_relat_1(A,B)) ) ),
    file(relat_1,k7_relat_1),
    []).

fof(fc4_funct_1,axiom,(
    ! [A,B] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( v1_relat_1(k7_relat_1(A,B))
        & v1_funct_1(k7_relat_1(A,B)) ) ) ),
    file(funct_1,fc4_funct_1),
    []).

fof(involutiveness_k1_funcop_1,axiom,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => k1_funcop_1(k1_funcop_1(A)) = A ) ),
    file(funcop_1,k1_funcop_1),
    []).

fof(rc1_funct_1,axiom,(
    ? [A] : 
      ( v1_relat_1(A)
      & v1_funct_1(A) ) ),
    file(funct_1,rc1_funct_1),
    []).

fof(t10_funcop_1,axiom,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ! [C] : k7_relat_1(k13_funct_3(A,B),C) = k13_funct_3(k7_relat_1(A,C),B) ) ) ),
    file(funcop_1,t10_funcop_1),
    []).

fof(t6_funcop_1,axiom,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => k13_funct_3(A,B) = k1_funcop_1(k13_funct_3(B,A)) ) ) ),
    file(funcop_1,t6_funcop_1),
    []).

fof(t7_funcop_1,axiom,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : k1_funcop_1(k7_relat_1(A,B)) = k7_relat_1(k1_funcop_1(A),B) ) ),
    file(funcop_1,t7_funcop_1),
    []).