let G be non empty multMagma ; :: thesis: for q being set

for z being Element of G

for f being {b_{1}} -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, FINSEQ_1:40

.= 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

for z being Element of G

for f being {b

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, FINSEQ_1:40

.= 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