let G be commutative Group; :: thesis: for A, B being non empty finite set
for FA being b1 -defined the carrier of G -valued total Function
for FB being b2 -defined the carrier of G -valued total Function
for FAB being b1 \/ b2 -defined the carrier of G -valued total Function st A misses B & FAB = FA +* FB holds
Product FAB = (Product FA) * (Product FB)

let A, B be non empty finite set ; :: thesis: for FA being A -defined the carrier of G -valued total Function
for FB being B -defined the carrier of G -valued total Function
for FAB being A \/ B -defined the carrier of G -valued total Function st A misses B & FAB = FA +* FB holds
Product FAB = (Product FA) * (Product FB)

let FA be A -defined the carrier of G -valued total Function; :: thesis: for FB being B -defined the carrier of G -valued total Function
for FAB being A \/ B -defined the carrier of G -valued total Function st A misses B & FAB = FA +* FB holds
Product FAB = (Product FA) * (Product FB)

let FB be B -defined the carrier of G -valued total Function; :: thesis: for FAB being A \/ B -defined the carrier of G -valued total Function st A misses B & FAB = FA +* FB holds
Product FAB = (Product FA) * (Product FB)

let FAB be A \/ B -defined the carrier of G -valued total Function; :: thesis: ( A misses B & FAB = FA +* FB implies Product FAB = (Product FA) * (Product FB) )
assume A1: A misses B ; :: thesis: ( not FAB = FA +* FB or Product FAB = (Product FA) * (Product FB) )
assume A2: FAB = FA +* FB ; :: thesis: Product FAB = (Product FA) * (Product FB)
consider fA being FinSequence of G such that
A3: ( Product FA = Product fA & fA = FA * () ) by Def1;
consider fB being FinSequence of G such that
A4: ( Product FB = Product fB & fB = FB * () ) by Def1;
set fAB = FAB * (canFS (A \/ B));
set cAB = () ^ ();
set uAB = canFS (A \/ B);
reconsider SGAB = Seg (card (A \/ B)) as non empty finite set ;
A5: ( (canFS A) ^ () is one-to-one onto FinSequence of A \/ B & dom (() ^ ()) = SGAB ) by ;
reconsider cAB = () ^ () as one-to-one onto FinSequence of A \/ B by ;
rng cAB c= A \/ B ;
then reconsider JcAB = cAB as Function of SGAB,(A \/ B) by ;
A6: dom (canFS (A \/ B)) = Seg (len (canFS (A \/ B))) by FINSEQ_1:def 3
.= SGAB by FINSEQ_1:93 ;
rng (canFS (A \/ B)) c= A \/ B ;
then reconsider KuAB = canFS (A \/ B) as Function of SGAB,(A \/ B) by ;
reconsider IuAB = (canFS (A \/ B)) " as Function of (A \/ B),SGAB by FINSEQ_1:95;
A7: rng (canFS (A \/ B)) = A \/ B by FUNCT_2:def 3;
then ( IuAB * KuAB = id SGAB & KuAB * IuAB = id (A \/ B) ) by FUNCT_2:29;
then A8: ( IuAB is one-to-one & IuAB is onto ) by FUNCT_2:23;
set p = IuAB * JcAB;
( IuAB * JcAB is onto & IuAB * JcAB is one-to-one ) by ;
then reconsider p = IuAB * JcAB as Permutation of SGAB ;
reconsider fAB = FAB * (canFS (A \/ B)) as FinSequence of G by Lm2;
A9: (canFS (A \/ B)) * p = (KuAB * IuAB) * JcAB by RELAT_1:36
.= (id (A \/ B)) * JcAB by
.= () ^ () by FUNCT_2:17 ;
A10: SGAB = dom fAB by Lm2;
A11: fA ^ fB = FAB * (() ^ ()) by A3, A4, Lm4, A1, A2
.= fAB * p by ;
thus Product FAB = Product fAB by Def1
.= Product (fA ^ fB) by
.= (Product FA) * (Product FB) by ; :: thesis: verum