let G be non empty multMagma ; :: thesis: for q being set
for z being Element of G
for f being {b1} -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 * () is FinSequence of G & dom (f * ()) = Seg () ) by Lm2;
reconsider g = f * () 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 . (() . 1) by
.= f . q by
.= z by ;
then <*z*> = f * () by ;
hence Product f = Product zz by Def1
.= z by GROUP_4:9 ;
:: thesis: verum