defpred S₁[ object , object ] 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)))) );

A1: now :: thesis: for ij being object st ij in the InternalRel of P holds
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)))) )

let ij be object ; :: 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 A2: 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₁( object ) -> 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
A3: for ij being object 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 A2, A3, MCART_1:21; :: thesis: verum

end;

A4: for z being object st z in the InternalRel of P holds
ex y being object st S₁[z,y]

proof

let z be object ; :: thesis: ( z in the InternalRel of P implies ex y being object st S₁[z,y] )
assume z in the InternalRel of P ; :: thesis: ex y being object st S₁[z,y]
then ex y being set st S₁[z,y] by A1;
hence ex y being object st S₁[z,y] ; :: thesis: verum

end;

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

proof

let z be object ; :: 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 ;
then consider i1, i2 being Element of P such that
z = [i2,i1] and
A6: A . z = IFEQ (i2,i1,(id the Sorts of (OAF . i1)),((bind (B,i1,i2)) ** (id the Sorts of (OAF . i1)))) by A5;

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

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

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

end;

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

hence A . z is Function by A6, 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 :: thesis: for i, j, k being Element of P st i >= j & j >= k holds
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 )

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
A7: i >= j and
A8: 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
A9: kl = [j,i] ;
kl in the InternalRel of P by A7, A9, ORDERS_2:def 5;
then consider i1, j1 being Element of P such that
A10: [j1,i1] = kl and
A11: A . kl = IFEQ (j1,i1,(id the Sorts of (OAF . i1)),((bind (B,i1,j1)) ** (id the Sorts of (OAF . i1)))) by A5;
A12: ( i1 = i & j1 = j ) by A9, A10, XTUPLE_0:1;
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 A10, A11, A12, 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 A10, A11, A12, 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
A13: lm = [k,j] ;
lm in the InternalRel of P by A8, A13, ORDERS_2:def 5;
then consider i2, j2 being Element of P such that
A14: [j2,i2] = lm and
A15: A . lm = IFEQ (j2,i2,(id the Sorts of (OAF . i2)),((bind (B,i2,j2)) ** (id the Sorts of (OAF . i2)))) by A5;
A16: ( j2 = k & i2 = j ) by A13, A14, XTUPLE_0:1;
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 A14, A15, A16, 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 A14, A15, A16, FUNCOP_1:def 8; :: thesis: verum

end;

end;

end;

then reconsider f2 = A . (k,j) as ManySortedFunction of (OAF . j),(OAF . k) ;
A17: 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
A18: i >= j and
A19: i <> j ; :: thesis: A . (j,i) = bind (B,i,j)
consider lm being set such that
A20: lm = [j,i] ;
lm in the InternalRel of P by A18, A20, ORDERS_2:def 5;
then consider i2, j2 being Element of P such that
A21: [j2,i2] = lm and
A22: A . lm = IFEQ (j2,i2,(id the Sorts of (OAF . i2)),((bind (B,i2,j2)) ** (id the Sorts of (OAF . i2)))) by A5;
( i2 = i & j2 = j ) by A20, A21, XTUPLE_0:1;
then A . (j,i) = (bind (B,i,j)) ** (id the Sorts of (OAF . i)) by A19, A21, A22, FUNCOP_1:def 8;
hence A . (j,i) = bind (B,i,j) by MSUALG_3:3; :: thesis: verum

end;

A23: 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 A24: ( i = j & j = k ) ; :: thesis: A . (k,i) = f2 ** f1

then f2 = id the Sorts of (OAF . j) by A14, A15, A16, 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 f1 = id the Sorts of (OAF . i) by A10, A11, A12, FUNCOP_1:def 8;
hence A . (k,i) = f2 ** f1 by A25, MSUALG_3:3; :: thesis: verum

end;

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

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

end;

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

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

end;

end;

end;

A30: 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
A31: lm = [j,i] ;
assume A32: 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 A31, ORDERS_2:def 5;
then consider i2, j2 being Element of P such that
A33: [j2,i2] = lm and
A34: A . lm = IFEQ (j2,i2,(id the Sorts of (OAF . i2)),((bind (B,i2,j2)) ** (id the Sorts of (OAF . i2)))) by A5;
( i2 = i & j2 = j ) by A31, A33, XTUPLE_0:1;
hence A . (j,i) = id the Sorts of (OAF . i) by A32, A33, A34, FUNCOP_1:def 8; :: thesis: verum

end;

f1 is_homomorphism OAF . i,OAF . j

proof

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

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

then A . (i,j) = id the Sorts of (OAF . i) by A30;
hence f1 is_homomorphism OAF . i,OAF . j by A35, 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 A7, A17;
hence f1 is_homomorphism OAF . i,OAF . j by A7, 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 A23; :: 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
A36: 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 A36, ORDERS_2:def 5;
then consider i1, j1 being Element of P such that
A37: [j1,i1] = kl and
A38: A . kl = IFEQ (j1,i1,(id the Sorts of (OAF . i1)),((bind (B,i1,j1)) ** (id the Sorts of (OAF . i1)))) by A5;
( i1 = i & j1 = j ) by A36, A37, XTUPLE_0:1;
hence A . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) by A37, A38; :: thesis: verum