let G1 be Group; :: thesis: for x being Element of G1 holds <*x*> " = <*(x ")*>

let x be Element of G1; :: thesis: <*x*> " = <*(x ")*>

reconsider G = <*G1*> as Group-like associative multMagma-Family of {1} ;

reconsider lF = <*x*>, p = <*(x ")*> as Element of product (Carrier G) by Def2;

A1: p . 1 = x " by FINSEQ_1:def 8;

A2: G . 1 = G1 by FINSEQ_1:def 8;

for i being set st i in {1} holds

ex H being Group ex z being Element of H st

( H = G . i & p . i = z " & z = lF . i )

let x be Element of G1; :: thesis: <*x*> " = <*(x ")*>

reconsider G = <*G1*> as Group-like associative multMagma-Family of {1} ;

reconsider lF = <*x*>, p = <*(x ")*> as Element of product (Carrier G) by Def2;

A1: p . 1 = x " by FINSEQ_1:def 8;

A2: G . 1 = G1 by FINSEQ_1:def 8;

for i being set st i in {1} holds

ex H being Group ex z being Element of H st

( H = G . i & p . i = z " & z = lF . i )

proof

hence
<*x*> " = <*(x ")*>
by Th7; :: thesis: verum
reconsider H = G . 1 as Group by FINSEQ_1:def 8;

reconsider z = p . 1 as Element of H by A1, FINSEQ_1:def 8;

let i be set ; :: thesis: ( i in {1} implies ex H being Group ex z being Element of H st

( H = G . i & p . i = z " & z = lF . i ) )

assume A3: i in {1} ; :: thesis: ex H being Group ex z being Element of H st

( H = G . i & p . i = z " & z = lF . i )

take H ; :: thesis: ex z being Element of H st

( H = G . i & p . i = z " & z = lF . i )

take z " ; :: thesis: ( H = G . i & p . i = (z ") " & z " = lF . i )

thus H = G . i by A3, TARSKI:def 1; :: thesis: ( p . i = (z ") " & z " = lF . i )

thus p . i = (z ") " by A3, TARSKI:def 1; :: thesis: z " = lF . i

i = 1 by A3, TARSKI:def 1;

hence z " = lF . i by A1, A2, FINSEQ_1:def 8; :: thesis: verum

end;reconsider z = p . 1 as Element of H by A1, FINSEQ_1:def 8;

let i be set ; :: thesis: ( i in {1} implies ex H being Group ex z being Element of H st

( H = G . i & p . i = z " & z = lF . i ) )

assume A3: i in {1} ; :: thesis: ex H being Group ex z being Element of H st

( H = G . i & p . i = z " & z = lF . i )

take H ; :: thesis: ex z being Element of H st

( H = G . i & p . i = z " & z = lF . i )

take z " ; :: thesis: ( H = G . i & p . i = (z ") " & z " = lF . i )

thus H = G . i by A3, TARSKI:def 1; :: thesis: ( p . i = (z ") " & z " = lF . i )

thus p . i = (z ") " by A3, TARSKI:def 1; :: thesis: z " = lF . i

i = 1 by A3, TARSKI:def 1;

hence z " = lF . i by A1, A2, FINSEQ_1:def 8; :: thesis: verum