let G be commutative Group; :: thesis: for A, B being non empty finite set

for FA being b_{1} -defined the carrier of G -valued total Function

for FB being b_{2} -defined the carrier of G -valued total Function

for FAB being b_{1} \/ b_{2} -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

for FA being b

for FB being b

for FAB being b

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