defpred S1[ 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 H1( 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 = H1(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 ; :: thesis: verum
end;
A4: for z being object st z in the InternalRel of P holds
ex y being object st S1[z,y]
proof
let z be object ; :: thesis: ( z in the InternalRel of P implies ex y being object st S1[z,y] )
assume z in the InternalRel of P ; :: thesis: ex y being object st S1[z,y]
then ex y being set st S1[z,y] by A1;
hence ex y being object st S1[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
S1[ij,A . ij] from 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 ; :: thesis: verum
end;
suppose i1 <> i2 ; :: thesis: A . z is Function
hence A . z is Function by ; :: 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 ;
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 ;
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 ; :: 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 ; :: 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 ;
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 ;
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 ; :: 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 ; :: 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 ;
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 ;
then A . (j,i) = (bind (B,i,j)) ** (id the Sorts of (OAF . i)) by ;
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 ;
hence A . (k,i) = f2 ** f1 by ; :: thesis: verum
end;
suppose A25: ( i = j & j <> k ) ; :: thesis: A . (k,i) = f2 ** f1
then f1 = id the Sorts of (OAF . i) by ;
hence A . (k,i) = f2 ** f1 by ; :: thesis: verum
end;
suppose A26: ( i <> j & j = k ) ; :: thesis: A . (k,i) = f2 ** f1
then f2 = id the Sorts of (OAF . j) by ;
hence A . (k,i) = f2 ** f1 by ; :: thesis: verum
end;
suppose A27: ( i <> j & j <> k ) ; :: thesis: A . (k,i) = f2 ** f1
then ( i > j & j > k ) by ;
then A28: i <> k by ORDERS_2:5;
f2 = (bind (B,j,k)) ** (id the Sorts of (OAF . j)) by ;
then A29: f2 = bind (B,j,k) by MSUALG_3:3;
f1 = (bind (B,i,j)) ** (id the Sorts of (OAF . i)) by ;
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 ; :: 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 ;
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 ;
hence A . (j,i) = id the Sorts of (OAF . i) by ; :: 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 ; :: thesis: verum
end;
suppose i <> j ; :: thesis: f1 is_homomorphism OAF . i,OAF . j
then A . (j,i) = bind (B,i,j) by ;
hence f1 is_homomorphism OAF . i,OAF . j by ; :: 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 ;
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 ;
hence A . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) by ; :: thesis: verum