let X be set ; :: thesis: for f1, f2, f3 being complex-valued ManySortedSet of X st ( for x being object st x in X holds
f1 . x = (f2 . x) * (f3 . x) ) holds
f1 = f2 (#) f3
let f1, f2, f3 be complex-valued ManySortedSet of X; :: thesis: ( ( for x being object st x in X holds
f1 . x = (f2 . x) * (f3 . x) ) implies f1 = f2 (#) f3 )
assume A1: for x being object st x in X holds
f1 . x = (f2 . x) * (f3 . x) ; :: thesis: f1 = f2 (#) f3
A2: ( dom f1 = X & dom f2 = X & dom f3 = X ) by PARTFUN1:def 2;
dom (f2 (#) f3) = (dom f2) /\ (dom f3) by VALUED_1:def 4;
hence f1 = f2 (#) f3 by A1, A2, VALUED_1:def 4; :: thesis: verum