reconsider T1 = the InternalRel of P as Relation of the carrier of P ;
consider A being non-empty MSAlgebra of S;
reconsider Z = the carrier of P --> A as ManySortedSet of the carrier of P ;
for i being set st i in the carrier of P holds
Z . i is non-empty MSAlgebra of S by FUNCOP_1:13;
then reconsider Z = Z as MSAlgebra-Family of the carrier of P,S by PRALG_2:def 12;
take Z ; :: thesis: ex F being ManySortedFunction of the InternalRel of P st
for i, j, k being Element of P st i >= j & j >= k holds
ex f1 being ManySortedFunction of (Z . i),(Z . j) ex f2 being ManySortedFunction of (Z . j),(Z . k) st
( f1 = F . j,i & f2 = F . k,j & F . k,i = f2 ** f1 & f1 is_homomorphism Z . i,Z . j )
set G = the InternalRel of P --> (id the Sorts of A);
reconsider G = the InternalRel of P --> (id the Sorts of A) as ManySortedFunction of the InternalRel of P ;
take G ; :: thesis: for i, j, k being Element of P st i >= j & j >= k holds
ex f1 being ManySortedFunction of (Z . i),(Z . j) ex f2 being ManySortedFunction of (Z . j),(Z . k) st
( f1 = G . j,i & f2 = G . k,j & G . k,i = f2 ** f1 & f1 is_homomorphism Z . i,Z . j )
let i, j, k be Element of P; :: thesis: ( i >= j & j >= k implies ex f1 being ManySortedFunction of (Z . i),(Z . j) ex f2 being ManySortedFunction of (Z . j),(Z . k) st
( f1 = G . j,i & f2 = G . k,j & G . k,i = f2 ** f1 & f1 is_homomorphism Z . i,Z . j ) )
A1: Z . j = A by FUNCOP_1:13;
Z . k = A by FUNCOP_1:13;
then consider F2 being ManySortedFunction of (Z . j),(Z . k) such that
A2: F2 = id the Sorts of A by A1;
assume ( i >= j & j >= k ) ; :: thesis: ex f1 being ManySortedFunction of (Z . i),(Z . j) ex f2 being ManySortedFunction of (Z . j),(Z . k) st
( f1 = G . j,i & f2 = G . k,j & G . k,i = f2 ** f1 & f1 is_homomorphism Z . i,Z . j )
then A3: ( [j,i] in the InternalRel of P & [k,j] in the InternalRel of P ) by ORDERS_2:def 9;
field T1 = the carrier of P by ORDERS_1:97;
then T1 is_transitive_in the carrier of P by RELAT_2:def 16;
then A4: [k,i] in T1 by A3, RELAT_2:def 8;
A5: Z . i = A by FUNCOP_1:13;
then consider F1 being ManySortedFunction of (Z . i),(Z . j) such that
A6: F1 = id the Sorts of A by A1;
take F1 ; :: thesis: ex f2 being ManySortedFunction of (Z . j),(Z . k) st
( F1 = G . j,i & f2 = G . k,j & G . k,i = f2 ** F1 & F1 is_homomorphism Z . i,Z . j )
take F2 ; :: thesis: ( F1 = G . j,i & F2 = G . k,j & G . k,i = F2 ** F1 & F1 is_homomorphism Z . i,Z . j )
F2 ** F1 = id the Sorts of A by A6, A2, MSUALG_3:3;
hence ( F1 = G . j,i & F2 = G . k,j & G . k,i = F2 ** F1 & F1 is_homomorphism Z . i,Z . j ) by A3, A5, A1, A6, A2, A4, FUNCOP_1:13, MSUALG_3:9; :: thesis: verum