let X, Y be set ; 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; ( 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)
; (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:40;
then A5:
dom ((Sgm X) * (Sgm Y)) = Seg (card Y9)
by A2, A4, RELAT_1:27;
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: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 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 ;
( ( y in rng L implies y in rng ((Sgm X) | Y) ) & ( y in rng ((Sgm X) | Y) implies y in rng L ) )assume
y in rng ((Sgm X) | Y)
;
y in rng Lthen 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;
verum end;
then A18:
rng L = rng ((Sgm X) | Y)
by TARSKI:2;
A19:
now for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len L & k1 = L . l & k2 = L . m holds
k1 < k2let l,
m,
k1,
k2 be
Nat;
( 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
;
k1 < k2
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 13;
hence
k1 < k2
by A1, A23, A24, A26, A28, A32, A33, FINSEQ_1:def 13;
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 A18, A19, FINSEQ_1:def 13; verum