consider A being non-empty MSAlgebra of S;
reconsider Z = the carrier of P --> A as ManySortedSet of ;
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 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 ;
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 ) )
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 A1: ( [j,i] in the InternalRel of P & [k,j] in the InternalRel of P ) by ORDERS_2:def 9;
A2: ( Z . i = A & Z . j = A & Z . k = A ) by FUNCOP_1:13;
then consider F1 being ManySortedFunction of (Z . i),(Z . j) such that
A3: F1 = id the Sorts of A ;
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 )
consider F2 being ManySortedFunction of (Z . j),(Z . k) such that
A4: F2 = id the Sorts of A by A2;
take F2 ; :: thesis: ( F1 = G . j,i & F2 = G . k,j & G . k,i = F2 ** F1 & F1 is_homomorphism Z . i,Z . j )
A5: F2 ** F1 = id the Sorts of A by A3, A4, MSUALG_3:3;
reconsider T1 = the InternalRel of P as Relation of the carrier of P ;
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 [k,i] in T1 by A1, RELAT_2:def 8;
hence ( F1 = G . j,i & F2 = G . k,j & G . k,i = F2 ** F1 & F1 is_homomorphism Z . i,Z . j ) by A1, A2, A3, A4, A5, FUNCOP_1:13, MSUALG_3:9; :: thesis: verum