let S be OrderSortedSign; 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 * ; 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; ( 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
; ( the Sorts of A #) . w1 c= ( the Sorts of A #) . w2
then A2:
len w1 = len w2
;
let x be object ; TARSKI:def 3 ( not x in ( the Sorts of A #) . w1 or x in ( the Sorts of A #) . w2 )
assume
x in ( the Sorts of A #) . w1
; 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 ;
( 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)
;
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;
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; verum