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);
A3: Y c= Seg (len (Sgm X)) by ;
then A4: rng (Sgm Y) = Y by FINSEQ_1:def 13;
dom (Sgm Y9) = Seg (card Y9) by ;
then A5: dom ((Sgm X) * (Sgm Y)) = Seg (card Y9) by ;
A6: rng (Sgm X) c= Seg k by ;
then A7: rng (Sgm X) c= NAT by XBOOLE_1:1;
reconsider M = (Sgm X) * (Sgm Y) as FinSequence by ;
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 ;
then A10: (Sgm Y) . x in Y by ;
y = (Sgm X) . ((Sgm Y) . x) by ;
hence y in rng ((Sgm X) | Y) by ; :: 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 ;
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 ;
x in dom (Sgm X) by ;
then A17: z in dom ((Sgm X) * (Sgm Y)) by ;
y = (Sgm X) . x by ;
then L . z = y by ;
hence y in rng L by ; :: thesis: verum
end;
then A18: rng L = rng ((Sgm X) | Y) by TARSKI:2;
A19: now :: thesis: for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len L & k1 = L . l & k2 = L . m holds
k1 < k2
let l, m, k1, k2 be Nat; :: 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 ;
then A25: l in dom L by ;
then A26: L . l = (Sgm X) . ((Sgm Y) . l) by FUNCT_1:12;
1 <= m by ;
then A27: m in dom L by ;
then A28: L . m = (Sgm X) . ((Sgm Y) . m) by FUNCT_1:12;
A29: (Sgm Y) . l in dom (Sgm X) by ;
m in dom (Sgm Y) by ;
then A30: m <= len (Sgm Y) by FINSEQ_3:25;
A31: (Sgm Y) . m in dom (Sgm X) by ;
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 ;
A33: K2 <= len (Sgm X) by ;
K1 < K2 by ;
hence k1 < k2 by ; :: 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;
hence (Sgm X) * (Sgm Y) = Sgm (rng ((Sgm X) | Y)) by ; :: thesis: verum