let X, Y be set ; :: thesis: for k being Element of NAT st X c= Seg k & Y c= dom (Sgm X) holds
(Sgm X) * (Sgm Y) = Sgm (rng ((Sgm X) | Y))
let k be Element of 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);
A3: Y c= Seg (len (Sgm X)) by A2, FINSEQ_1:def 3;
then A4: rng (Sgm Y) = Y by FINSEQ_1:def 13;
dom (Sgm Y9) = Seg (card Y9) by A3, FINSEQ_3:45;
then A5: dom ((Sgm X) * (Sgm Y)) = Seg (card Y9) by A2, A4, RELAT_1:46;
A6: rng (Sgm X) c= Seg k by A1, FINSEQ_1:def 13;
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:45;
then rng M c= NAT by A7, XBOOLE_1:1;
then reconsider L = (Sgm X) * (Sgm Y) as FinSequence of NAT by FINSEQ_1:def 4;

now

let y be set ; :: 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 set such that
A8: x in dom L and
A9: y = L . x by FUNCT_1:def 5;
x in dom (Sgm Y) by A8, FUNCT_1:21;
then A10: (Sgm Y) . x in Y by A4, FUNCT_1:def 5;
y = (Sgm X) . ((Sgm Y) . x) by A8, A9, FUNCT_1:22;
hence y in rng ((Sgm X) | Y) by A2, A10, FUNCT_1:73; :: thesis: verum

end;

assume y in rng ((Sgm X) | Y) ; :: thesis: y in rng L
then consider x being set such that
A11: x in dom ((Sgm X) | Y) and
A12: y = ((Sgm X) | Y) . x by FUNCT_1:def 5;
A13: x in (dom (Sgm X)) /\ Y by A11, RELAT_1:90;
then A14: x in Y by XBOOLE_0:def 4;
then consider z being set such that
A15: z in dom (Sgm Y) and
A16: x = (Sgm Y) . z by A4, FUNCT_1:def 5;
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:21;
y = (Sgm X) . x by A12, A14, FUNCT_1:72;
then L . z = y by A16, A17, FUNCT_1:22;
hence y in rng L by A17, FUNCT_1:def 5; :: thesis: verum

end;

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

A19: now

let l, m, k1, k2 be natural number ; :: thesis: ( 1 <= l & l < m & m <= len L & k1 = L . l & k2 = L . m implies k1 < k2 )
assume that
A20: 1 <= l and
A21: l < m and
A22: m <= len L and
A23: k1 = L . l and
A24: k2 = L . m ; :: thesis: k1 < k2
l <= len L by A21, A22, XXREAL_0:2;
then A25: l in dom L by A20, FINSEQ_3:27;
then A26: L . l = (Sgm X) . ((Sgm Y) . l) by FUNCT_1:22;
1 <= m by A20, A21, XXREAL_0:2;
then A27: m in dom L by A22, FINSEQ_3:27;
then A28: L . m = (Sgm X) . ((Sgm Y) . m) by FUNCT_1:22;
A29: (Sgm Y) . l in dom (Sgm X) by A25, FUNCT_1:21;
m in dom (Sgm Y) by A27, FUNCT_1:21;
then A30: m <= len (Sgm Y) by FINSEQ_3:27;
A31: (Sgm Y) . m in dom (Sgm X) by A27, FUNCT_1:21;
reconsider l = l, m = m as Element of NAT by ORDINAL1:def 13;
reconsider K1 = (Sgm Y) . l, K2 = (Sgm Y) . m as Element of NAT ;
A32: 1 <= K1 by A29, FINSEQ_3:27;
A33: K2 <= len (Sgm X) by A31, FINSEQ_3:27;
K1 < K2 by A3, A20, A21, A30, FINSEQ_1:def 13;
hence k1 < k2 by A1, A23, A24, A26, A28, A32, A33, FINSEQ_1:def 13; :: thesis: verum

end;

rng ((Sgm X) | Y) c= rng (Sgm X) by RELAT_1:99;
then rng ((Sgm X) | Y) c= Seg k by A6, XBOOLE_1:1;
hence (Sgm X) * (Sgm Y) = Sgm (rng ((Sgm X) | Y)) by A18, A19, FINSEQ_1:def 13; :: thesis: verum