let f, g be FinSequence of COMPLEX ; :: thesis: for i being object holds (f (#) g) . i = (f . i) * (g . i)
let i be object ; :: thesis: (f (#) g) . i = (f . i) * (g . i)

per cases ( i in dom (f (#) g) or not i in dom (f (#) g) ) ;

suppose i in dom (f (#) g) ; :: thesis: (f (#) g) . i = (f . i) * (g . i)

hence (f (#) g) . i = (f . i) * (g . i) by VALUED_1:def 4; :: thesis: verum

end;

suppose B1: not i in dom (f (#) g) ; :: thesis: (f (#) g) . i = (f . i) * (g . i)

then not i in (dom f) /\ (dom g) by VALUED_1:def 4;
then ( not i in dom f or not i in dom g ) by XBOOLE_0:def 4;
then ( ( f . i = {} or g . i = {} ) & (f (#) g) . i = {} ) by B1, FUNCT_1:def 2;
hence (f (#) g) . i = (f . i) * (g . i) ; :: thesis: verum

end;

end;