reconsider T1 = the InternalRel of P as Relation of the carrier of P ;
set A = the non-empty MSAlgebra over S;
reconsider Z = the carrier of P --> the non-empty MSAlgebra over S as ManySortedSet of the carrier of P ;
for i being object st i in the carrier of P holds
Z . i is non-empty MSAlgebra over S by FUNCOP_1:7;
then reconsider Z = Z as MSAlgebra-Family of the carrier of P,S by PRALG_2:def 5;
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 the non-empty MSAlgebra over S);
reconsider G = the InternalRel of P --> (id the Sorts of the non-empty MSAlgebra over S) 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 ) )
consider F2 being ManySortedFunction of (Z . j),(Z . k) such that
A2: F2 = id the Sorts of the non-empty MSAlgebra over S ;
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 5;
field T1 = the carrier of P by ORDERS_1:12;
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;
consider F1 being ManySortedFunction of (Z . i),(Z . j) such that
A6: F1 = id the Sorts of the non-empty MSAlgebra over S ;
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 the non-empty MSAlgebra over S 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, A6, A2, A4, FUNCOP_1:7, MSUALG_3:9; :: thesis: verum