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))
A3: Y c= Seg (len (Sgm X)) by A2, FINSEQ_1:def 3;
set M = (Sgm X) * (Sgm Y);
reconsider Y' = Y as finite set by A2;
A4: dom (Sgm Y') = Seg (card Y') by A3, FINSEQ_3:45;
A5: rng (Sgm Y) = Y by A3, FINSEQ_1:def 13;
then dom ((Sgm X) * (Sgm Y)) = Seg (card Y') by A2, A4, RELAT_1:46;
then reconsider M = (Sgm X) * (Sgm Y) as FinSequence by FINSEQ_1:def 2;
A6: ( rng (Sgm X) c= Seg k & Seg k c= NAT ) by A1, FINSEQ_1:def 13;
then A7: rng (Sgm X) c= NAT by XBOOLE_1:1;
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;
set R = rng ((Sgm X) | Y);
rng ((Sgm X) | Y) c= rng (Sgm X) by RELAT_1:99;
then A8: rng ((Sgm X) | Y) c= Seg k by A6, XBOOLE_1:1;

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

end;

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

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
A17: 1 <= l and
A18: l < m and
A19: m <= len L and
A20: k1 = L . l and
A21: k2 = L . m ; :: thesis: k1 < k2
( l <= len L & 1 <= m ) by A17, A18, A19, XXREAL_0:2;
then A22: ( l in dom L & m in dom L ) by A17, A19, FINSEQ_3:27;
then A23: ( L . l = (Sgm X) . ((Sgm Y) . l) & L . m = (Sgm X) . ((Sgm Y) . m) ) by FUNCT_1:22;
A24: ( l in dom (Sgm Y) & (Sgm Y) . l in dom (Sgm X) & m in dom (Sgm Y) & (Sgm Y) . m in dom (Sgm X) ) by A22, FUNCT_1:21;
then A25: ( 1 <= l & l <= len (Sgm Y) & 1 <= m & m <= len (Sgm Y) ) by FINSEQ_3:27;
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 ;
A26: K1 < K2 by A3, A18, A25, FINSEQ_1:def 13;
( 1 <= K1 & K1 <= len (Sgm X) & 1 <= K2 & K2 <= len (Sgm X) ) by A24, FINSEQ_3:27;
hence k1 < k2 by A1, A20, A21, A23, A26, FINSEQ_1:def 13; :: thesis: verum

end;

hence (Sgm X) * (Sgm Y) = Sgm (rng ((Sgm X) | Y)) by A8, A16, FINSEQ_1:def 13; :: thesis: verum