let G be non empty multMagma ; :: thesis: for q being set
for z being Element of G
for f being {b₁} -defined the carrier of G -valued total Function st f = q .--> z holds
Product f = z
let q be set ; :: thesis: for z being Element of G
for f being {q} -defined the carrier of G -valued total Function st f = q .--> z holds
Product f = z
let z be Element of G; :: thesis: for f being {q} -defined the carrier of G -valued total Function st f = q .--> z holds
Product f = z
let f be {q} -defined the carrier of G -valued total Function; :: thesis: ( f = q .--> z implies Product f = z )
assume A1: f = q .--> z ; :: thesis: Product f = z
set zz = <*z*>;
rng <*z*> = {z} by FINSEQ_1:38;
then reconsider zz = <*z*> as FinSequence of G by FINSEQ_1:def 4;
A2: ( f * (canFS {q}) is FinSequence of G & dom (f * (canFS {q})) = Seg (card {q}) ) by Lm2;
reconsider g = f * (canFS {q}) as FinSequence of G by Lm2;
A3: card {q} = 1 by CARD_1:30;
then dom g = Seg 1 by Lm2;
then A4: len g = 1 by FINSEQ_1:def 3;
A5: canFS {q} = <*q*> by FINSEQ_1:94;
A6: q in {q} by TARSKI:def 1;
A7: 1 in dom g by A2, A3;
g . 1 = f . ((canFS {q}) . 1) by FUNCT_1:12, A7
.= f . q by A5
.= z by A1, FUNCOP_1:7, A6 ;
then <*z*> = f * (canFS {q}) by A4, FINSEQ_1:40;
hence Product f = Product zz by Def1
.= z by GROUP_4:9 ;
:: thesis: verum