let V, W be non empty set ; for f, g being V -valued FinSequence
for l being Function of V,W holds l * (f ^ g) = (l * f) ^ (l * g)
let f, g be V -valued FinSequence; for l being Function of V,W holds l * (f ^ g) = (l * f) ^ (l * g)
let l be Function of V,W; l * (f ^ g) = (l * f) ^ (l * g)
A1:
dom l = V
by FUNCT_2:def 1;
A2:
rng f c= V
;
A3:
rng g c= V
;
A4:
rng (f ^ g) = (rng f) \/ (rng g)
by FINSEQ_1:31;
A5: dom (l * f) =
dom f
by A1, A2, RELAT_1:27
.=
Seg (len f)
by FINSEQ_1:def 3
;
then A6:
len (l * f) = len f
by FINSEQ_1:def 3;
dom (l * g) =
dom g
by A1, A3, RELAT_1:27
.=
Seg (len g)
by FINSEQ_1:def 3
;
then A7:
len (l * g) = len g
by FINSEQ_1:def 3;
A8: dom (f ^ g) =
Seg (len (f ^ g))
by FINSEQ_1:def 3
.=
Seg ((len f) + (len g))
by FINSEQ_1:22
;
A9: len ((l * f) ^ (l * g)) =
(len (l * f)) + (len (l * g))
by FINSEQ_1:22
.=
(len f) + (len g)
by A5, A7, FINSEQ_1:def 3
;
A10:
dom ((l * f) ^ (l * g)) = Seg ((len f) + (len g))
by A9, FINSEQ_1:def 3;
hence
l * (f ^ g) = (l * f) ^ (l * g)
by A1, A4, A8, A10, FUNCT_1:2, RELAT_1:27; verum