% Mizar problem: t29_algspec1,algspec1,505,39 
fof(t29_algspec1,conjecture,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ( r1_tarski(A,B)
           => ! [C] : 
                ( m1_algspec1(C,A)
               => ? [D] : 
                    ( m1_algspec1(D,B)
                    & r1_tarski(C,D) ) ) ) ) ) ),
    inference(mizar_bg_added,[status(thm)],[dt_k1_funct_4,dt_k1_zfmisc_1,dt_m1_algspec1,dt_m1_subset_1,existence_m1_algspec1,existence_m1_subset_1,idempotence_k1_funct_4,rc1_funct_1,reflexivity_r1_partfun1,reflexivity_r1_tarski,symmetry_r1_partfun1,t131_partfun1,t26_funct_4,t28_algspec1,t3_subset,t79_funct_4]),
    [file(algspec1,t29_algspec1)]).

fof(dt_k1_funct_4,axiom,(
    ! [A,B] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_relat_1(B)
        & v1_funct_1(B) )
     => ( v1_relat_1(k1_funct_4(A,B))
        & v1_funct_1(k1_funct_4(A,B)) ) ) ),
    file(funct_4,k1_funct_4),
    []).

fof(dt_k1_zfmisc_1,axiom,(
    $true ),
    file(zfmisc_1,k1_zfmisc_1),
    []).

fof(dt_m1_algspec1,axiom,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( m1_algspec1(B,A)
         => ( v1_relat_1(B)
            & v1_funct_1(B) ) ) ) ),
    file(algspec1,m1_algspec1),
    []).

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

fof(existence_m1_algspec1,axiom,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ? [B] : m1_algspec1(B,A) ) ),
    file(algspec1,m1_algspec1),
    []).

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

fof(idempotence_k1_funct_4,axiom,(
    ! [A,B] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_relat_1(B)
        & v1_funct_1(B) )
     => k1_funct_4(A,A) = A ) ),
    file(funct_4,k1_funct_4),
    []).

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

fof(reflexivity_r1_partfun1,axiom,(
    ! [A,B] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_relat_1(B)
        & v1_funct_1(B) )
     => r1_partfun1(A,A) ) ),
    file(partfun1,r1_partfun1),
    []).

fof(reflexivity_r1_tarski,axiom,(
    ! [A,B] : r1_tarski(A,A) ),
    file(tarski,r1_tarski),
    []).

fof(symmetry_r1_partfun1,axiom,(
    ! [A,B] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_relat_1(B)
        & v1_funct_1(B) )
     => ( r1_partfun1(A,B)
       => r1_partfun1(B,A) ) ) ),
    file(partfun1,r1_partfun1),
    []).

fof(t131_partfun1,axiom,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ( r1_partfun1(A,B)
          <=> ? [C] : 
                ( v1_relat_1(C)
                & v1_funct_1(C)
                & r1_tarski(A,C)
                & r1_tarski(B,C) ) ) ) ) ),
    file(partfun1,t131_partfun1),
    []).

fof(t26_funct_4,axiom,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => r1_tarski(A,k1_funct_4(B,A)) ) ) ),
    file(funct_4,t26_funct_4),
    []).

fof(t28_algspec1,axiom,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ( r1_partfun1(A,B)
           => ! [C] : 
                ( m1_algspec1(C,A)
               => ! [D] : 
                    ( m1_algspec1(D,B)
                   => m1_algspec1(k1_funct_4(C,D),k1_funct_4(A,B)) ) ) ) ) ) ),
    file(algspec1,t28_algspec1),
    []).

fof(t3_subset,axiom,(
    ! [A,B] : 
      ( m1_subset_1(A,k1_zfmisc_1(B))
    <=> r1_tarski(A,B) ) ),
    file(subset,t3_subset),
    []).

fof(t79_funct_4,axiom,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ( r1_tarski(A,B)
           => ( k1_funct_4(A,B) = B
              & k1_funct_4(B,A) = B ) ) ) ) ),
    file(funct_4,t79_funct_4),
    []).