defpred S₁[ set , set ] means ex i, j being Element of P st
( $1 = [j,i] & $2 = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) );

now

let ij be set ; :: thesis: ( ij in the InternalRel of P implies ex x being set ex i1, i2 being Element of P st
( ij = [i2,i1] & x = IFEQ (i2,i1,(id the Sorts of (OAF . i1)),((bind (B,i1,i2)) ** (id the Sorts of (OAF . i1)))) ) )
assume A1: ij in the InternalRel of P ; :: thesis: ex x being set ex i1, i2 being Element of P st
( ij = [i2,i1] & x = IFEQ (i2,i1,(id the Sorts of (OAF . i1)),((bind (B,i1,i2)) ** (id the Sorts of (OAF . i1)))) )
then reconsider i2 = ij `1 , i1 = ij `2 as Element of P by MCART_1:10;
reconsider i1 = i1, i2 = i2 as Element of P ;
deffunc H₁( set ) -> set = IFEQ (i2,i1,(id the Sorts of (OAF . i1)),((bind (B,i1,i2)) ** (id the Sorts of (OAF . i1))));
consider A being ManySortedSet of the InternalRel of P such that
A2: for ij being set st ij in the InternalRel of P holds
A . ij = H₁(ij) from PBOOLE:sch 4();
take x = A . ij; :: thesis: ex i1, i2 being Element of P st
( ij = [i2,i1] & x = IFEQ (i2,i1,(id the Sorts of (OAF . i1)),((bind (B,i1,i2)) ** (id the Sorts of (OAF . i1)))) )
take i1 = i1; :: thesis: ex i2 being Element of P st
( ij = [i2,i1] & x = IFEQ (i2,i1,(id the Sorts of (OAF . i1)),((bind (B,i1,i2)) ** (id the Sorts of (OAF . i1)))) )
take i2 = i2; :: thesis: ( ij = [i2,i1] & x = IFEQ (i2,i1,(id the Sorts of (OAF . i1)),((bind (B,i1,i2)) ** (id the Sorts of (OAF . i1)))) )
thus ( ij = [i2,i1] & x = IFEQ (i2,i1,(id the Sorts of (OAF . i1)),((bind (B,i1,i2)) ** (id the Sorts of (OAF . i1)))) ) by A1, A2, MCART_1:21; :: thesis: verum

end;

then A3: for z being set st z in the InternalRel of P holds
ex y being set st S₁[z,y] ;
consider A being ManySortedSet of the InternalRel of P such that
A4: for ij being set st ij in the InternalRel of P holds
S₁[ij,A . ij] from PBOOLE:sch 3(A3);
for z being set st z in dom A holds
A . z is Function

proof

let z be set ; :: thesis: ( z in dom A implies A . z is Function )
assume z in dom A ; :: thesis: A . z is Function
then z in the InternalRel of P by PARTFUN1:def 2;
then consider i1, i2 being Element of P such that
z = [i2,i1] and
A5: A . z = IFEQ (i2,i1,(id the Sorts of (OAF . i1)),((bind (B,i1,i2)) ** (id the Sorts of (OAF . i1)))) by A4;

per cases ( i1 = i2 or i1 <> i2 ) ;

suppose i1 = i2 ; :: thesis: A . z is Function

hence A . z is Function by A5, FUNCOP_1:def 8; :: thesis: verum

end;

suppose i1 <> i2 ; :: thesis: A . z is Function

hence A . z is Function by A5, FUNCOP_1:def 8; :: thesis: verum

end;

end;

end;

then reconsider A = A as ManySortedFunction of the InternalRel of P by FUNCOP_1:def 6;

now

let i, j, k be Element of P; :: thesis: ( i >= j & j >= k implies ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . k) st
( f1 = A . (j,i) & f2 = A . (k,j) & A . (k,i) = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j ) )
assume that
A6: i >= j and
A7: j >= k ; :: thesis: ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . k) st
( f1 = A . (j,i) & f2 = A . (k,j) & A . (k,i) = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j )
consider kl being set such that
A8: kl = [j,i] ;
kl in the InternalRel of P by A6, A8, ORDERS_2:def 5;
then consider i1, j1 being Element of P such that
A9: [j1,i1] = kl and
A10: A . kl = IFEQ (j1,i1,(id the Sorts of (OAF . i1)),((bind (B,i1,j1)) ** (id the Sorts of (OAF . i1)))) by A4;
A11: ( i1 = i & j1 = j ) by A8, A9, ZFMISC_1:27;
A . (j,i) is ManySortedFunction of (OAF . i),(OAF . j)

proof

per cases ( i = j or i <> j ) ;

suppose i = j ; :: thesis: A . (j,i) is ManySortedFunction of (OAF . i),(OAF . j)

hence A . (j,i) is ManySortedFunction of (OAF . i),(OAF . j) by A9, A10, A11, FUNCOP_1:def 8; :: thesis: verum

end;

suppose i <> j ; :: thesis: A . (j,i) is ManySortedFunction of (OAF . i),(OAF . j)

hence A . (j,i) is ManySortedFunction of (OAF . i),(OAF . j) by A9, A10, A11, FUNCOP_1:def 8; :: thesis: verum

end;

end;

end;

then reconsider f1 = A . (j,i) as ManySortedFunction of (OAF . i),(OAF . j) ;
consider lm being set such that
A12: lm = [k,j] ;
lm in the InternalRel of P by A7, A12, ORDERS_2:def 5;
then consider i2, j2 being Element of P such that
A13: [j2,i2] = lm and
A14: A . lm = IFEQ (j2,i2,(id the Sorts of (OAF . i2)),((bind (B,i2,j2)) ** (id the Sorts of (OAF . i2)))) by A4;
A15: ( j2 = k & i2 = j ) by A12, A13, ZFMISC_1:27;
A . (k,j) is ManySortedFunction of (OAF . j),(OAF . k)

proof

per cases ( j = k or j <> k ) ;

suppose j = k ; :: thesis: A . (k,j) is ManySortedFunction of (OAF . j),(OAF . k)

hence A . (k,j) is ManySortedFunction of (OAF . j),(OAF . k) by A13, A14, A15, FUNCOP_1:def 8; :: thesis: verum

end;

suppose j <> k ; :: thesis: A . (k,j) is ManySortedFunction of (OAF . j),(OAF . k)

hence A . (k,j) is ManySortedFunction of (OAF . j),(OAF . k) by A13, A14, A15, FUNCOP_1:def 8; :: thesis: verum

end;

end;

end;

then reconsider f2 = A . (k,j) as ManySortedFunction of (OAF . j),(OAF . k) ;
A16: for i, j being Element of P st i >= j & i <> j holds
A . (j,i) = bind (B,i,j)

proof

let i, j be Element of P; :: thesis: ( i >= j & i <> j implies A . (j,i) = bind (B,i,j) )
assume that
A17: i >= j and
A18: i <> j ; :: thesis: A . (j,i) = bind (B,i,j)
consider lm being set such that
A19: lm = [j,i] ;
lm in the InternalRel of P by A17, A19, ORDERS_2:def 5;
then consider i2, j2 being Element of P such that
A20: [j2,i2] = lm and
A21: A . lm = IFEQ (j2,i2,(id the Sorts of (OAF . i2)),((bind (B,i2,j2)) ** (id the Sorts of (OAF . i2)))) by A4;
( i2 = i & j2 = j ) by A19, A20, ZFMISC_1:27;
then A . (j,i) = (bind (B,i,j)) ** (id the Sorts of (OAF . i)) by A18, A20, A21, FUNCOP_1:def 8;
hence A . (j,i) = bind (B,i,j) by MSUALG_3:3; :: thesis: verum

end;

A22: A . (k,i) = f2 ** f1

proof

per cases ( ( i = j & j = k ) or ( i = j & j <> k ) or ( i <> j & j = k ) or ( i <> j & j <> k ) ) ;

suppose A23: ( i = j & j = k ) ; :: thesis: A . (k,i) = f2 ** f1

then f2 = id the Sorts of (OAF . j) by A13, A14, A15, FUNCOP_1:def 8;
hence A . (k,i) = f2 ** f1 by A23, MSUALG_3:3; :: thesis: verum

end;

suppose A24: ( i = j & j <> k ) ; :: thesis: A . (k,i) = f2 ** f1

then f1 = id the Sorts of (OAF . i) by A9, A10, A11, FUNCOP_1:def 8;
hence A . (k,i) = f2 ** f1 by A24, MSUALG_3:3; :: thesis: verum

end;

suppose A25: ( i <> j & j = k ) ; :: thesis: A . (k,i) = f2 ** f1

then f2 = id the Sorts of (OAF . j) by A13, A14, A15, FUNCOP_1:def 8;
hence A . (k,i) = f2 ** f1 by A25, MSUALG_3:4; :: thesis: verum

end;

suppose A26: ( i <> j & j <> k ) ; :: thesis: A . (k,i) = f2 ** f1

then ( i > j & j > k ) by A6, A7, ORDERS_2:def 6;
then A27: i <> k by ORDERS_2:5;
f2 = (bind (B,j,k)) ** (id the Sorts of (OAF . j)) by A13, A14, A15, A26, FUNCOP_1:def 8;
then A28: f2 = bind (B,j,k) by MSUALG_3:3;
f1 = (bind (B,i,j)) ** (id the Sorts of (OAF . i)) by A9, A10, A11, A26, FUNCOP_1:def 8;
then f1 = bind (B,i,j) by MSUALG_3:3;
then f2 ** f1 = bind (B,i,k) by A6, A7, A28, Th1;
hence A . (k,i) = f2 ** f1 by A6, A7, A16, A27, ORDERS_2:3; :: thesis: verum

end;

end;

end;

A29: for i, j being Element of P st i = j holds
A . (j,i) = id the Sorts of (OAF . i)

proof

let i, j be Element of P; :: thesis: ( i = j implies A . (j,i) = id the Sorts of (OAF . i) )
consider lm being set such that
A30: lm = [j,i] ;
assume A31: i = j ; :: thesis: A . (j,i) = id the Sorts of (OAF . i)
then i >= j by ORDERS_2:1;
then lm in the InternalRel of P by A30, ORDERS_2:def 5;
then consider i2, j2 being Element of P such that
A32: [j2,i2] = lm and
A33: A . lm = IFEQ (j2,i2,(id the Sorts of (OAF . i2)),((bind (B,i2,j2)) ** (id the Sorts of (OAF . i2)))) by A4;
( i2 = i & j2 = j ) by A30, A32, ZFMISC_1:27;
hence A . (j,i) = id the Sorts of (OAF . i) by A31, A32, A33, FUNCOP_1:def 8; :: thesis: verum

end;

f1 is_homomorphism OAF . i,OAF . j

proof

per cases ( i = j or i <> j ) ;

suppose A34: i = j ; :: thesis: f1 is_homomorphism OAF . i,OAF . j

then A . (i,j) = id the Sorts of (OAF . i) by A29;
hence f1 is_homomorphism OAF . i,OAF . j by A34, MSUALG_3:9; :: thesis: verum

end;

suppose i <> j ; :: thesis: f1 is_homomorphism OAF . i,OAF . j

then A . (j,i) = bind (B,i,j) by A6, A16;
hence f1 is_homomorphism OAF . i,OAF . j by A6, Th2; :: thesis: verum

end;

end;

end;

hence ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . k) st
( f1 = A . (j,i) & f2 = A . (k,j) & A . (k,i) = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j ) by A22; :: thesis: verum

end;

then reconsider A = A as Binding of OAF by Def2;
take A ; :: thesis: for i, j being Element of P st i >= j holds
A . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i))))
let i, j be Element of P; :: thesis: ( i >= j implies A . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) )
consider kl being set such that
A35: kl = [j,i] ;
assume i >= j ; :: thesis: A . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i))))
then kl in the InternalRel of P by A35, ORDERS_2:def 5;
then consider i1, j1 being Element of P such that
A36: [j1,i1] = kl and
A37: A . kl = IFEQ (j1,i1,(id the Sorts of (OAF . i1)),((bind (B,i1,j1)) ** (id the Sorts of (OAF . i1)))) by A4;
( i1 = i & j1 = j ) by A35, A36, ZFMISC_1:27;
hence A . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) by A36, A37; :: thesis: verum