defpred S_{1}[ 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)))) );

ex y being object st S_{1}[z,y]

A5: for ij being object st ij in the InternalRel of P holds

S_{1}[ij,A . ij]
from PBOOLE:sch 3(A4);

for z being object st z in dom A holds

A . z is Function

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

( $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)))) )

A4:
for z being object st z 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_{1}( 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_{1}(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;( 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

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

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

ex y being object st S

proof

consider A being ManySortedSet of the InternalRel of P such that
let z be object ; :: thesis: ( z in the InternalRel of P implies ex y being object st S_{1}[z,y] )

assume z in the InternalRel of P ; :: thesis: ex y being object st S_{1}[z,y]

then ex y being set st S_{1}[z,y]
by A1;

hence ex y being object st S_{1}[z,y]
; :: thesis: verum

end;assume z in the InternalRel of P ; :: thesis: ex y being object st S

then ex y being set st S

hence ex y being object st S

A5: for ij being object st ij in the InternalRel of P holds

S

for z being object st z in dom A holds

A . z is Function

proof

then reconsider A = A as ManySortedFunction of the InternalRel of P by FUNCOP_1:def 6;
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;

end;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;

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 )

then reconsider A = A as Binding of OAF by Def2;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)

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)

A17: for i, j being Element of P st i >= j & i <> j holds

A . (j,i) = bind (B,i,j)

A . (j,i) = id the Sorts of (OAF . i)

( 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;( 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
end;

then reconsider f1 = A . (j,i) as ManySortedFunction of (OAF . i),(OAF . j) ;per cases
( i = j or i <> j )
;

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;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;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
end;

then reconsider f2 = A . (k,j) as ManySortedFunction of (OAF . j),(OAF . k) ;per cases
( j = k or j <> k )
;

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;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;A17: for i, j being Element of P st i >= j & i <> j holds

A . (j,i) = bind (B,i,j)

proof

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

proof
end;

A30:
for i, j being Element of P st i = j holds per cases
( ( i = j & j = k ) or ( i = j & j <> k ) or ( i <> j & j = k ) or ( i <> j & j <> k ) )
;

end;

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;hence A . (k,i) = f2 ** f1 by A24, MSUALG_3:3; :: thesis: verum

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;hence A . (k,i) = f2 ** f1 by A25, MSUALG_3:3; :: thesis: verum

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;hence A . (k,i) = f2 ** f1 by A26, MSUALG_3:4; :: thesis: verum

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;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

A . (j,i) = id the Sorts of (OAF . i)

proof

f1 is_homomorphism OAF . i,OAF . j
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;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

proof
end;

hence
ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . k) st per cases
( i = j or i <> j )
;

end;

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;hence f1 is_homomorphism OAF . i,OAF . j by A35, MSUALG_3:9; :: thesis: verum

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;hence f1 is_homomorphism OAF . i,OAF . j by A7, Th2; :: thesis: verum

( f1 = A . (j,i) & f2 = A . (k,j) & A . (k,i) = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j ) by A23; :: thesis: verum

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