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
by Def7;
let x be set ; 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 PBOOLE:def 19;
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 set 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:31
.=
dom (the Sorts of A * w2)
by Lm1
;
for y being set st y in dom (the Sorts of A * w2) holds
g . y in (the Sorts of A * w2) . y
proof
let y be
set ;
( 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:23;
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:23;
reconsider s1 =
w1 . y,
s2 =
w2 . y as
SortSymbol of
S by A8, A10, PARTFUN1:27;
s1 <= s2
by A1, A8, Def7;
then A12:
the
Sorts of
A . (w1 . y) c= the
Sorts of
A . (w2 . y)
by Def19;
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, PBOOLE:def 19; verum