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;