let S be OrderSortedSign; :: thesis: for w1, w2 being Element of the carrier of S *
for A being OSAlgebra of S st w1 <= w2 holds
( the Sorts of A #) . w1 c= ( the Sorts of A #) . w2
let w1, w2 be Element of the carrier of S * ; :: thesis: for A being OSAlgebra of S st w1 <= w2 holds
( the Sorts of A #) . w1 c= ( the Sorts of A #) . w2
let A be OSAlgebra of S; :: thesis: ( w1 <= w2 implies ( the Sorts of A #) . w1 c= ( the Sorts of A #) . w2 )
set iw1 = the Sorts of A * w1;
set iw2 = the Sorts of A * w2;
assume A1: w1 <= w2 ; :: thesis: ( the Sorts of A #) . w1 c= ( the Sorts of A #) . w2
then A2: len w1 = len w2 ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ( the Sorts of A #) . w1 or x in ( the Sorts of A #) . w2 )
assume x in ( the Sorts of A #) . w1 ; :: thesis: x in ( the Sorts of A #) . w2
then x in product ( the Sorts of A * w1) by FINSEQ_2:def 5;
then consider g being Function such that
A3: x = g and
A4: dom g = dom ( the Sorts of A * w1) and
A5: for y being object st y in dom ( the Sorts of A * w1) holds
g . y in ( the Sorts of A * w1) . y by CARD_3:def 5;
A6: dom ( the Sorts of A * w1) = dom w1 by Lm1
.= dom w2 by A2, FINSEQ_3:29
.= dom ( the Sorts of A * w2) by Lm1 ;
for y being object st y in dom ( the Sorts of A * w2) holds
g . y in ( the Sorts of A * w2) . y

proof

let y be object ; :: thesis: ( y in dom ( the Sorts of A * w2) implies g . y in ( the Sorts of A * w2) . y )
assume A7: y in dom ( the Sorts of A * w2) ; :: thesis: g . y in ( the Sorts of A * w2) . y
A8: y in dom w1 by A6, A7, Lm1;
then A9: ( the Sorts of A * w1) . y = the Sorts of A . (w1 . y) by FUNCT_1:13;
A10: y in dom w2 by A7, Lm1;
then A11: ( the Sorts of A * w2) . y = the Sorts of A . (w2 . y) by FUNCT_1:13;
reconsider s1 = w1 . y, s2 = w2 . y as SortSymbol of S by A8, A10, PARTFUN1:4;
s1 <= s2 by A1, A8;
then A12: the Sorts of A . (w1 . y) c= the Sorts of A . (w2 . y) by Def17;
g . y in ( the Sorts of A * w1) . y by A5, A6, A7;
hence g . y in ( the Sorts of A * w2) . y by A9, A11, A12; :: thesis: verum

end;

then g in product ( the Sorts of A * w2) by A4, A6, CARD_3:def 5;
hence x in ( the Sorts of A #) . w2 by A3, FINSEQ_2:def 5; :: thesis: verum