let X be set ; :: thesis: for b1, b2 being complex-valued finite-support ManySortedSet of X st support b1 = support b2 holds
Product (b1 (#) b2) = (Product b1) * (Product b2)
let b1, b2 be complex-valued finite-support ManySortedSet of X; :: thesis: ( support b1 = support b2 implies Product (b1 (#) b2) = (Product b1) * (Product b2) )
set b0 = b1 (#) b2;
assume A1: support b1 = support b2 ; :: thesis: Product (b1 (#) b2) = (Product b1) * (Product b2)
A2: support (b1 (#) b2) = support b1 by A1, Th15;
A3: support (b1 (#) b2) = support b2 by A1, Th15;
consider f0 being FinSequence of COMPLEX such that
A4: Product (b1 (#) b2) = Product f0 and
A5: f0 = (b1 (#) b2) * (canFS (support (b1 (#) b2))) by NAT_3:def 5;
consider f1 being FinSequence of COMPLEX such that
A6: Product b1 = Product f1 and
A7: f1 = b1 * (canFS (support b1)) by NAT_3:def 5;
consider f2 being FinSequence of COMPLEX such that
A8: Product b2 = Product f2 and
A9: f2 = b2 * (canFS (support b2)) by NAT_3:def 5;
A10: f1 is len f1 -element by CARD_1:def 7;
A11: f2 is len f2 -element by CARD_1:def 7;
A12: dom ((b1 (#) b2) * (canFS (support (b1 (#) b2)))) = dom (canFS (support (b1 (#) b2))) by Th13;
then A13: dom f0 = dom f1 by A2, A5, A7, Th13;
then A14: len f0 = len f1 by FINSEQ_3:29;
A15: dom f0 = dom f2 by A3, A5, A9, A12, Th13;
then A16: len f0 = len f2 by FINSEQ_3:29;
A17: dom f0 = (dom f1) /\ (dom f2) by A13, A15;
for c being object st c in dom f0 holds
f0 . c = (f1 . c) * (f2 . c)

proof

let c be object ; :: thesis: ( c in dom f0 implies f0 . c = (f1 . c) * (f2 . c) )
assume A18: c in dom f0 ; :: thesis: f0 . c = (f1 . c) * (f2 . c)
set x = (canFS (support (b1 (#) b2))) . c;
A19: f1 . c = b1 . ((canFS (support (b1 (#) b2))) . c) by A2, A7, A13, A18, FUNCT_1:12;
A20: f2 . c = b2 . ((canFS (support (b1 (#) b2))) . c) by A3, A9, A15, A18, FUNCT_1:12;
thus f0 . c = (b1 (#) b2) . ((canFS (support (b1 (#) b2))) . c) by A5, A18, FUNCT_1:12
.= (f1 . c) * (f2 . c) by A19, A20, VALUED_1:5 ; :: thesis: verum

end;

then f0 = f1 (#) f2 by A17, VALUED_1:def 4;
hence Product (b1 (#) b2) = (Product b1) * (Product b2) by A4, A6, A8, A10, A11, A14, A16, NEWTON04:63; :: thesis: verum