let f1, f2 be complex-valued Function; :: thesis: for c being object holds (f1 (#) f2) . c = (f1 . c) * (f2 . c)
let c be object ; :: thesis: (f1 (#) f2) . c = (f1 . c) * (f2 . c)
A1: dom (f1 (#) f2) = (dom f1) /\ (dom f2) by Def4;

per cases ( c in dom (f1 (#) f2) or not c in dom (f1 (#) f2) ) ;

suppose c in dom (f1 (#) f2) ; :: thesis: (f1 (#) f2) . c = (f1 . c) * (f2 . c)

hence (f1 (#) f2) . c = (f1 . c) * (f2 . c) by Def4; :: thesis: verum

end;

suppose A2: not c in dom (f1 (#) f2) ; :: thesis: (f1 (#) f2) . c = (f1 . c) * (f2 . c)

then ( not c in dom f1 or not c in dom f2 ) by A1, XBOOLE_0:def 4;
then ( f1 . c = 0 or f2 . c = 0 ) by FUNCT_1:def 2;
hence (f1 (#) f2) . c = (f1 . c) * (f2 . c) by A2, FUNCT_1:def 2; :: thesis: verum

end;

end;