let X be set ; :: thesis: for a, b being bag of X st support a misses support b holds
Product (a + b) = (Product a) * (Product b)
let a, b be bag of X; :: thesis: ( support a misses support b implies Product (a + b) = (Product a) * (Product b) )
set ab = a + b;
set Pa = Product a;
set Pb = Product b;
set Pab = Product (a + b);
set sab = support (a + b);
set sa = support a;
set sb = support b;
set ca = canFS (support a);
set cb = canFS (support b);
set cg = (canFS (support a)) ^ (canFS (support b));
set cf = canFS (support (a + b));
set p = (((canFS (support a)) ^ (canFS (support b))) ") * (canFS (support (a + b)));
A1: rng (canFS (support (a + b))) = support (a + b) by FUNCT_2:def 3;
assume support a misses support b ; :: thesis: Product (a + b) = (Product a) * (Product b)
then A2: (support a) /\ (support b) = {} by XBOOLE_0:def 7;
A3: rng (canFS (support a)) = support a by FUNCT_2:def 3;
A4: support (a + b) = (support a) \/ (support b) by PRE_POLY:38;
A5: rng (canFS (support b)) = support b by FUNCT_2:def 3;
then A6: rng ((canFS (support a)) ^ (canFS (support b))) = support (a + b) by A4, A3, FINSEQ_1:44;
A7: ( len (canFS (support b)) = card (support b) & len (canFS (support a)) = card (support a) ) by UPROOTS:5;
then A8: len ((canFS (support a)) ^ (canFS (support b))) = ((card (support a)) + (card (support b))) - (card {}) by FINSEQ_1:35
.= card (support (a + b)) by A2, A4, CARD_2:64 ;
then A9: (canFS (support a)) ^ (canFS (support b)) is one-to-one by A6, FINSEQ_4:77;
then A10: dom (((canFS (support a)) ^ (canFS (support b))) ") = support (a + b) by A6, FUNCT_1:55;
then A11: rng ((((canFS (support a)) ^ (canFS (support b))) ") * (canFS (support (a + b)))) = rng (((canFS (support a)) ^ (canFS (support b))) ") by A1, RELAT_1:47;
dom ((canFS (support a)) ^ (canFS (support b))) = Seg (card (support (a + b))) by A8, FINSEQ_1:def 3;
then A12: rng (((canFS (support a)) ^ (canFS (support b))) ") = Seg (card (support (a + b))) by A9, FUNCT_1:55;
consider fa being FinSequence of COMPLEX such that
A13: Product a = Product fa and
A14: fa = a * (canFS (support a)) by Def5;
consider fb being FinSequence of COMPLEX such that
A15: Product b = Product fb and
A16: fb = b * (canFS (support b)) by Def5;
set g = fa ^ fb;
consider f being FinSequence of COMPLEX such that
A17: Product (a + b) = Product f and
A18: f = (a + b) * (canFS (support (a + b))) by Def5;
dom a = X by PARTFUN1:def 4;
then A19: dom (canFS (support a)) = dom fa by A14, A3, RELAT_1:46;
then A20: len (canFS (support a)) = len fa by FINSEQ_3:31;
len (canFS (support (a + b))) = card (support (a + b)) by UPROOTS:5;
then A21: dom (canFS (support (a + b))) = Seg (card (support (a + b))) by FINSEQ_1:def 3;
then A22: dom ((((canFS (support a)) ^ (canFS (support b))) ") * (canFS (support (a + b)))) = Seg (card (support (a + b))) by A1, A10, RELAT_1:46;
A23: dom (a + b) = X by PARTFUN1:def 4;
then A24: dom f = Seg (card (support (a + b))) by A18, A21, A1, RELAT_1:46;
dom b = X by PARTFUN1:def 4;
then dom (canFS (support b)) = dom fb by A16, A5, RELAT_1:46;
then A25: len (canFS (support b)) = len fb by FINSEQ_3:31;
then len (fa ^ fb) = ((card (support a)) + (card (support b))) - (card {}) by A7, A20, FINSEQ_1:35
.= card (support (a + b)) by A2, A4, CARD_2:64 ;
then A26: dom (fa ^ fb) = Seg (card (support (a + b))) by FINSEQ_1:def 3;
then reconsider p = (((canFS (support a)) ^ (canFS (support b))) ") * (canFS (support (a + b))) as Function of (dom (fa ^ fb)),(dom (fa ^ fb)) by A12, A22, A11, FUNCT_2:3;
p is onto by A12, A26, A11, FUNCT_2:def 3;
then reconsider p = p as Permutation of (dom (fa ^ fb)) by A9;
A27: dom ((fa ^ fb) * p) = Seg (card (support (a + b))) by A12, A22, A26, A11, RELAT_1:46;
A28: len ((canFS (support a)) ^ (canFS (support b))) = (len (canFS (support a))) + (len (canFS (support b))) by FINSEQ_1:35;

now

let x be set ; :: thesis: ( x in dom f implies f . b₁ = ((fa ^ fb) * p) . b₁ )
set cgx = (((canFS (support a)) ^ (canFS (support b))) ") . ((canFS (support (a + b))) . x);
assume A29: x in dom f ; :: thesis: f . b₁ = ((fa ^ fb) * p) . b₁
then A30: ((fa ^ fb) * p) . x = (fa ^ fb) . (p . x) by A24, A27, FUNCT_1:22
.= (fa ^ fb) . ((((canFS (support a)) ^ (canFS (support b))) ") . ((canFS (support (a + b))) . x)) by A21, A24, A29, FUNCT_1:23 ;
A31: (canFS (support (a + b))) . x in support (a + b) by A21, A1, A24, A29, FUNCT_1:12;
then consider d being set such that
A32: d in dom ((canFS (support a)) ^ (canFS (support b))) and
A33: ((canFS (support a)) ^ (canFS (support b))) . d = (canFS (support (a + b))) . x by A6, FUNCT_1:def 5;
(((canFS (support a)) ^ (canFS (support b))) ") . ((canFS (support (a + b))) . x) in Seg (card (support (a + b))) by A10, A12, A31, FUNCT_1:12;
then reconsider cgx = (((canFS (support a)) ^ (canFS (support b))) ") . ((canFS (support (a + b))) . x) as natural number ;
reconsider cgxN = cgx as Nat ;
A34: cgx = d by A9, A32, A33, FUNCT_1:56;
then A35: 1 <= cgxN by A32, FINSEQ_3:27;
A36: cgxN <= (len fa) + (len fb) by A20, A25, A28, A32, A34, FINSEQ_3:27;

per cases ( (canFS (support (a + b))) . x in support a or (canFS (support (a + b))) . x in support b ) by A4, A31, XBOOLE_0:def 3;

suppose (canFS (support (a + b))) . x in support a ; :: thesis: f . b₁ = ((fa ^ fb) * p) . b₁

then A37: not (canFS (support (a + b))) . x in support b by A2, XBOOLE_0:def 4;

now

A38: cgx - (len (canFS (support a))) <= ((len (canFS (support a))) + (len (canFS (support b)))) - (len (canFS (support a))) by A20, A25, A36, XREAL_1:11;
assume len fa < cgx ; :: thesis: contradiction
then A39: (len fa) + 1 <= cgx by NAT_1:13;
then A40: ((len (canFS (support a))) + 1) - (len (canFS (support a))) <= cgx - (len (canFS (support a))) by A20, XREAL_1:11;
then cgx - (len (canFS (support a))) is Element of NAT by INT_1:16;
then A41: cgx - (len (canFS (support a))) in dom (canFS (support b)) by A40, A38, FINSEQ_3:27;
((canFS (support a)) ^ (canFS (support b))) . cgxN = (canFS (support b)) . (cgx - (len (canFS (support a)))) by A20, A25, A36, A39, FINSEQ_1:36;
hence contradiction by A5, A33, A34, A37, A41, FUNCT_1:12; :: thesis: verum

end;

then A42: cgxN in dom fa by A35, FINSEQ_3:27;
then A43: ((canFS (support a)) ^ (canFS (support b))) . cgx = (canFS (support a)) . cgx by A19, FINSEQ_1:def 7;
A44: (fa ^ fb) . cgx = fa . cgxN by A42, FINSEQ_1:def 7
.= a . ((canFS (support (a + b))) . x) by A14, A19, A33, A34, A42, A43, FUNCT_1:23 ;
thus f . x = (a + b) . ((canFS (support (a + b))) . x) by A18, A29, FUNCT_1:22
.= (a . ((canFS (support (a + b))) . x)) + (b . ((canFS (support (a + b))) . x)) by PRE_POLY:def 5
.= (a . ((canFS (support (a + b))) . x)) + 0 by A37, PRE_POLY:def 7
.= ((fa ^ fb) * p) . x by A30, A44 ; :: thesis: verum

end;

suppose A45: (canFS (support (a + b))) . x in support b ; :: thesis: f . b₁ = ((fa ^ fb) * p) . b₁

A46: now

assume (len fa) + 1 > cgx ; :: thesis: contradiction
then cgx <= len fa by NAT_1:13;
then A47: cgx in dom (canFS (support a)) by A19, A35, FINSEQ_3:27;
then (canFS (support a)) . cgx in support a by A3, FUNCT_1:12;
then ((canFS (support a)) ^ (canFS (support b))) . cgxN in support a by A47, FINSEQ_1:def 7;
hence contradiction by A2, A33, A34, A45, XBOOLE_0:def 4; :: thesis: verum

end;

then A48: ((canFS (support a)) ^ (canFS (support b))) . cgx = (canFS (support b)) . (cgx - (len (canFS (support a)))) by A20, A25, A36, FINSEQ_1:36;
A49: cgx - (len (canFS (support a))) <= ((len (canFS (support a))) + (len (canFS (support b)))) - (len (canFS (support a))) by A20, A25, A36, XREAL_1:11;
A50: ((len (canFS (support a))) + 1) - (len (canFS (support a))) <= cgx - (len (canFS (support a))) by A20, A46, XREAL_1:11;
then cgxN - (len (canFS (support a))) in NAT by INT_1:16;
then A51: cgxN - (len (canFS (support a))) in dom (canFS (support b)) by A49, A50, FINSEQ_3:27;
A52: (fa ^ fb) . cgx = fb . (cgxN - (len fa)) by A36, A46, FINSEQ_1:36
.= b . ((canFS (support (a + b))) . x) by A16, A20, A33, A34, A48, A51, FUNCT_1:23 ;
A53: not (canFS (support (a + b))) . x in support a by A2, A45, XBOOLE_0:def 4;
thus f . x = (a + b) . ((canFS (support (a + b))) . x) by A18, A29, FUNCT_1:22
.= (a . ((canFS (support (a + b))) . x)) + (b . ((canFS (support (a + b))) . x)) by PRE_POLY:def 5
.= 0 + (b . ((canFS (support (a + b))) . x)) by A53, PRE_POLY:def 7
.= ((fa ^ fb) * p) . x by A30, A52 ; :: thesis: verum

end;

end;

end;

then A54: f = (fa ^ fb) * p by A18, A21, A1, A23, A27, FUNCT_1:9, RELAT_1:46;
thus Product (a + b) = multcomplex $$ f by A17, RVSUM_1:def 14
.= multcomplex $$ (fa ^ fb) by A54, FINSOP_1:8
.= Product (fa ^ fb) by RVSUM_1:def 14
.= (Product a) * (Product b) by A13, A15, RVSUM_1:127 ; :: thesis: verum