let X, Y be set ; :: thesis: for k being Nat st X c= Seg k & Y c= dom (Sgm X) holds
(Sgm X) * (Sgm Y) = Sgm (rng ((Sgm X) | Y))
let k be Nat; :: thesis: ( X c= Seg k & Y c= dom (Sgm X) implies (Sgm X) * (Sgm Y) = Sgm (rng ((Sgm X) | Y)) )
assume that
A1: X c= Seg k and
A2: Y c= dom (Sgm X) ; :: thesis: (Sgm X) * (Sgm Y) = Sgm (rng ((Sgm X) | Y))
reconsider Y9 = Y as finite set by A2;
set M = (Sgm X) * (Sgm Y);
set R = rng ((Sgm X) | Y);
Y c= Seg (len (Sgm X)) by A2, FINSEQ_1:def 3;
then a3: Y is included_in_Seg ;
then A4: rng (Sgm Y) = Y by FINSEQ_1:def 14;
dom (Sgm Y9) = Seg (card Y9) by a3, FINSEQ_3:40;
then A5: dom ((Sgm X) * (Sgm Y)) = Seg (card Y9) by A2, A4, RELAT_1:27;
a1: X is included_in_Seg by A1;
then A6: rng (Sgm X) c= Seg k by A1, FINSEQ_1:def 14;
then A7: rng (Sgm X) c= NAT by XBOOLE_1:1;
reconsider M = (Sgm X) * (Sgm Y) as FinSequence by A5, FINSEQ_1:def 2;
rng M c= rng (Sgm X) by RELAT_1:26;
then rng M c= NAT by A7;
then reconsider L = (Sgm X) * (Sgm Y) as FinSequence of NAT by FINSEQ_1:def 4;

now :: thesis: for y being object holds
( ( y in rng L implies y in rng ((Sgm X) | Y) ) & ( y in rng ((Sgm X) | Y) implies y in rng L ) )

let y be object ; :: thesis: ( ( y in rng L implies y in rng ((Sgm X) | Y) ) & ( y in rng ((Sgm X) | Y) implies y in rng L ) )

hereby :: thesis: ( y in rng ((Sgm X) | Y) implies y in rng L )

assume y in rng L ; :: thesis: y in rng ((Sgm X) | Y)
then consider x being object such that
A8: x in dom L and
A9: y = L . x by FUNCT_1:def 3;
x in dom (Sgm Y) by A8, FUNCT_1:11;
then A10: (Sgm Y) . x in Y by A4, FUNCT_1:def 3;
y = (Sgm X) . ((Sgm Y) . x) by A8, A9, FUNCT_1:12;
hence y in rng ((Sgm X) | Y) by A2, A10, FUNCT_1:50; :: thesis: verum

end;

assume y in rng ((Sgm X) | Y) ; :: thesis: y in rng L
then consider x being object such that
A11: x in dom ((Sgm X) | Y) and
A12: y = ((Sgm X) | Y) . x by FUNCT_1:def 3;
A13: x in (dom (Sgm X)) /\ Y by A11, RELAT_1:61;
then A14: x in Y by XBOOLE_0:def 4;
then consider z being object such that
A15: z in dom (Sgm Y) and
A16: x = (Sgm Y) . z by A4, FUNCT_1:def 3;
x in dom (Sgm X) by A13, XBOOLE_0:def 4;
then A17: z in dom ((Sgm X) * (Sgm Y)) by A15, A16, FUNCT_1:11;
y = (Sgm X) . x by A12, A14, FUNCT_1:49;
then L . z = y by A16, A17, FUNCT_1:12;
hence y in rng L by A17, FUNCT_1:def 3; :: thesis: verum

end;

then A18: rng L = rng ((Sgm X) | Y) by TARSKI:2;

A19: now :: thesis: for l, m being Nat st 1 <= l & l < m & m <= len L holds
L . l < L . m

let l, m be Nat; :: thesis: ( 1 <= l & l < m & m <= len L implies L . l < L . m )
assume that
A20: 1 <= l and
A21: l < m and
A22: m <= len L ; :: thesis: L . l < L . m
set k1 = L . l;
set k2 = L . m;
l <= len L by A21, A22, XXREAL_0:2;
then A25: l in dom L by A20, FINSEQ_3:25;
then A26: L . l = (Sgm X) . ((Sgm Y) . l) by FUNCT_1:12;
1 <= m by A20, A21, XXREAL_0:2;
then A27: m in dom L by A22, FINSEQ_3:25;
then A28: L . m = (Sgm X) . ((Sgm Y) . m) by FUNCT_1:12;
A29: (Sgm Y) . l in dom (Sgm X) by A25, FUNCT_1:11;
m in dom (Sgm Y) by A27, FUNCT_1:11;
then A30: m <= len (Sgm Y) by FINSEQ_3:25;
A31: (Sgm Y) . m in dom (Sgm X) by A27, FUNCT_1:11;
reconsider l = l, m = m as Element of NAT by ORDINAL1:def 12;
reconsider K1 = (Sgm Y) . l, K2 = (Sgm Y) . m as Element of NAT by ORDINAL1:def 12;
A32: 1 <= K1 by A29, FINSEQ_3:25;
A33: K2 <= len (Sgm X) by A31, FINSEQ_3:25;
K1 < K2 by a3, A20, A21, A30, FINSEQ_1:def 14;
hence L . l < L . m by a1, A26, A28, A32, A33, FINSEQ_1:def 14; :: thesis: verum

end;

rng ((Sgm X) | Y) c= rng (Sgm X) by RELAT_1:70;
then rng ((Sgm X) | Y) c= Seg k by A6;
then rng ((Sgm X) | Y) is included_in_Seg ;
hence (Sgm X) * (Sgm Y) = Sgm (rng ((Sgm X) | Y)) by A18, A19, FINSEQ_1:def 14; :: thesis: verum