let V, W be non empty set ; :: thesis: 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; :: thesis: for l being Function of V,W holds l * (f ^ g) = (l * f) ^ (l * g)
let l be Function of V,W; :: thesis: 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;
now :: thesis: for k being object st k in dom (l * (f ^ g)) holds
(l * (f ^ g)) . k = ((l * f) ^ (l * g)) . k
let k be object ; :: thesis: ( k in dom (l * (f ^ g)) implies (l * (f ^ g)) . b1 = ((l * f) ^ (l * g)) . b1 )
assume A11: k in dom (l * (f ^ g)) ; :: thesis: (l * (f ^ g)) . b1 = ((l * f) ^ (l * g)) . b1
then reconsider i = k as Nat ;
A12: i in dom (f ^ g) by A1, A4, A11, RELAT_1:27;
per cases ( i in dom f or ex n being Nat st
( n in dom g & i = (len f) + n ) ) by A12, FINSEQ_1:25;
suppose A13: i in dom f ; :: thesis: (l * (f ^ g)) . b1 = ((l * f) ^ (l * g)) . b1
then A14: i in dom (l * f) by A1, A2, RELAT_1:27;
thus (l * (f ^ g)) . k = l . ((f ^ g) . i) by A11, FUNCT_1:12
.= l . (f . i) by A13, FINSEQ_1:def 7
.= (l * f) . i by A13, FUNCT_1:13
.= ((l * f) ^ (l * g)) . k by A14, FINSEQ_1:def 7 ; :: thesis: verum
end;
suppose ex n being Nat st
( n in dom g & i = (len f) + n ) ; :: thesis: (l * (f ^ g)) . b1 = ((l * f) ^ (l * g)) . b1
then consider n being Nat such that
A15: ( n in dom g & i = (len f) + n ) ;
A16: n in dom (l * g) by A1, A3, A15, RELAT_1:27;
thus (l * (f ^ g)) . k = l . ((f ^ g) . i) by A11, FUNCT_1:12
.= l . (g . n) by A15, FINSEQ_1:def 7
.= (l * g) . n by A15, FUNCT_1:13
.= ((l * f) ^ (l * g)) . k by A6, A15, A16, FINSEQ_1:def 7 ; :: thesis: verum
end;
end;
end;
hence l * (f ^ g) = (l * f) ^ (l * g) by A1, A4, A8, A10, FUNCT_1:2, RELAT_1:27; :: thesis: verum