let G be commutative Group; :: thesis: for A, B being non empty finite set
for FA being b₁ -defined the carrier of G -valued total Function
for FB being b₂ -defined the carrier of G -valued total Function
for FAB being b₁ \/ b₂ -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 * (canFS A) ) by Def1;
consider fB being FinSequence of G such that
A4: ( Product FB = Product fB & fB = FB * (canFS B) ) by Def1;
set fAB = FAB * (canFS (A \/ B));
set cAB = (canFS A) ^ (canFS B);
set uAB = canFS (A \/ B);
reconsider SGAB = Seg (card (A \/ B)) as non empty finite set ;
A5: ( (canFS A) ^ (canFS B) is one-to-one onto FinSequence of A \/ B & dom ((canFS A) ^ (canFS B)) = SGAB ) by Lm3, A1;
reconsider cAB = (canFS A) ^ (canFS B) as one-to-one onto FinSequence of A \/ B by Lm3, A1;
rng cAB c= A \/ B ;
then reconsider JcAB = cAB as Function of SGAB,(A \/ B) by FUNCT_2:2, A5;
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 FUNCT_2:2, A6;
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 A8, FUNCT_2:27;
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 A7, FUNCT_2:29
.= (canFS A) ^ (canFS B) by FUNCT_2:17 ;
A10: SGAB = dom fAB by Lm2;
A11: fA ^ fB = FAB * ((canFS A) ^ (canFS B)) by A3, A4, Lm4, A1, A2
.= fAB * p by RELAT_1:36, A9 ;
thus Product FAB = Product fAB by Def1
.= Product (fA ^ fB) by A10, A11, UPROOTS:16
.= (Product FA) * (Product FB) by A3, A4, GROUP_4:5 ; :: thesis: verum