let K be non empty addLoopStr ; for f, g, h, w being FinSequence of K st len f = len g & len h = len w holds
(f ^ h) + (g ^ w) = (f + g) ^ (h + w)
let f, g, h, w be FinSequence of K; ( len f = len g & len h = len w implies (f ^ h) + (g ^ w) = (f + g) ^ (h + w) )
assume that
A1:
len f = len g
and
A2:
len h = len w
; (f ^ h) + (g ^ w) = (f + g) ^ (h + w)
set KK = the carrier of K;
reconsider H = h, W = w as Element of (len h) -tuples_on the carrier of K by A2, FINSEQ_2:92;
reconsider F = f, G = g as Element of (len f) -tuples_on the carrier of K by A1, FINSEQ_2:92;
reconsider FH = F ^ H, GW = G ^ W, Th36W = (F + G) ^ (H + W) as Tuple of (len f) + (len h), the carrier of K ;
reconsider FH = FH, GW = GW, Th36W = Th36W as Element of ((len f) + (len h)) -tuples_on the carrier of K by FINSEQ_2:131;
now for i being Nat st i in Seg ((len f) + (len h)) holds
(FH + GW) . i = Th36W . ilet i be
Nat;
( i in Seg ((len f) + (len h)) implies (FH + GW) . i = Th36W . i )assume A3:
i in Seg ((len f) + (len h))
;
(FH + GW) . i = Th36W . iA4:
i in dom FH
by A3, FINSEQ_2:124;
now (FH + GW) . i = Th36W . iper cases
( i in dom f or ex n being Nat st
( n in dom h & i = (len f) + n ) )
by A4, FINSEQ_1:25;
suppose A5:
i in dom f
;
(FH + GW) . i = Th36W . iA6:
(
rng f c= the
carrier of
K &
rng g c= the
carrier of
K )
by RELAT_1:def 19;
A7:
dom (F + G) = Seg (len f)
by FINSEQ_2:124;
A8:
f . i in rng f
by A5, FUNCT_1:def 3;
A9:
dom F = Seg (len f)
by FINSEQ_2:124;
A10:
dom G = Seg (len f)
by FINSEQ_2:124;
then
g . i in rng g
by A5, A9, FUNCT_1:def 3;
then reconsider fi =
f . i,
gi =
g . i as
Element of
K by A8, A6;
A11:
FH . i = fi
by A5, FINSEQ_1:def 7;
GW . i = gi
by A5, A9, A10, FINSEQ_1:def 7;
hence (FH + GW) . i =
fi + gi
by A3, A11, FVSUM_1:18
.=
(F + G) . i
by A5, A9, FVSUM_1:18
.=
Th36W . i
by A5, A9, A7, FINSEQ_1:def 7
;
verum end; suppose
ex
n being
Nat st
(
n in dom h &
i = (len f) + n )
;
(FH + GW) . i = Th36W . ithen consider n being
Nat such that A12:
n in dom h
and A13:
i = (len f) + n
;
A14:
h . n in rng h
by A12, FUNCT_1:def 3;
A15:
(
rng h c= the
carrier of
K &
rng w c= the
carrier of
K )
by RELAT_1:def 19;
A16:
dom H = Seg (len h)
by FINSEQ_2:124;
A17:
dom W = Seg (len h)
by FINSEQ_2:124;
then
w . n in rng w
by A12, A16, FUNCT_1:def 3;
then reconsider hn =
h . n,
wn =
w . n as
Element of
K by A14, A15;
A18:
FH . i = hn
by A12, A13, FINSEQ_1:def 7;
A19:
(
dom (H + W) = Seg (len h) &
len (F + G) = len f )
by CARD_1:def 7, FINSEQ_2:124;
GW . i = wn
by A1, A12, A13, A16, A17, FINSEQ_1:def 7;
hence (FH + GW) . i =
hn + wn
by A3, A18, FVSUM_1:18
.=
(H + W) . n
by A12, A16, FVSUM_1:18
.=
Th36W . i
by A12, A13, A16, A19, FINSEQ_1:def 7
;
verum end; hence
(FH + GW) . i = Th36W . i
;
verum end;
hence
(f ^ h) + (g ^ w) = (f + g) ^ (h + w)
by FINSEQ_2:119; verum