let a be Complex; :: thesis: for f, g being complex-valued FinSequence holds a (#) (f ^ g) = (a (#) f) ^ (a (#) g)
let f, g be complex-valued FinSequence; :: thesis: a (#) (f ^ g) = (a (#) f) ^ (a (#) g)
A0: ( dom (a (#) (f ^ g)) = dom (f ^ g) & dom (a (#) f) = dom f & dom (a (#) g) = dom g ) by VALUED_1:def 5;
then A1: ( len (a (#) (f ^ g)) = len (f ^ g) & len (a (#) f) = len f & len (a (#) g) = len g ) by FINSEQ_3:29;
then len (a (#) (f ^ g)) = (len (a (#) f)) + (len (a (#) g)) by FINSEQ_1:22
.= len ((a (#) f) ^ (a (#) g)) by FINSEQ_1:22 ;
then A2: dom (a (#) (f ^ g)) = dom ((a (#) f) ^ (a (#) g)) by FINSEQ_3:29;
for x being object st x in dom (a (#) (f ^ g)) holds
(a (#) (f ^ g)) . x = ((a (#) f) ^ (a (#) g)) . x
proof
let x be object ; :: thesis: ( x in dom (a (#) (f ^ g)) implies (a (#) (f ^ g)) . x = ((a (#) f) ^ (a (#) g)) . x )
assume B1: x in dom (a (#) (f ^ g)) ; :: thesis: (a (#) (f ^ g)) . x = ((a (#) f) ^ (a (#) g)) . x
per cases ( x in dom f or not x in dom f ) ;
suppose C1: x in dom f ; :: thesis: (a (#) (f ^ g)) . x = ((a (#) f) ^ (a (#) g)) . x
then C2: x in dom (a (#) f) by VALUED_1:def 5;
then ((a (#) f) ^ (a (#) g)) . x = (a (#) f) . x by FINSEQ_1:def 7
.= a * (f . x) by C2, VALUED_1:def 5
.= a * ((f ^ g) . x) by C1, FINSEQ_1:def 7
.= (a (#) (f ^ g)) . x by B1, VALUED_1:def 5 ;
hence (a (#) (f ^ g)) . x = ((a (#) f) ^ (a (#) g)) . x ; :: thesis: verum
end;
suppose C0: not x in dom f ; :: thesis: (a (#) (f ^ g)) . x = ((a (#) f) ^ (a (#) g)) . x
x in dom (f ^ g) by VALUED_1:def 5, B1;
then consider n being Nat such that
C2: ( n in dom g & x = (len f) + n ) by C0, FINSEQ_1:25;
((a (#) f) ^ (a (#) g)) . ((len f) + n) = (a (#) g) . n by A0, A1, C2, FINSEQ_1:def 7
.= a * (g . n) by A0, C2, VALUED_1:def 5
.= a * ((f ^ g) . ((len f) + n)) by C2, FINSEQ_1:def 7
.= (a (#) (f ^ g)) . x by C2, B1, VALUED_1:def 5 ;
hence (a (#) (f ^ g)) . x = ((a (#) f) ^ (a (#) g)) . x by C2; :: thesis: verum
end;
end;
end;
hence a (#) (f ^ g) = (a (#) f) ^ (a (#) g) by A2, FUNCT_1:2; :: thesis: verum