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;
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

reconsider H = G . 1 as Group ;
reconsider z = p . 1 as Element of H ;
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 ; :: thesis: verum

end;

hence <*x*> " = <*(x ")*> by Th7; :: thesis: verum