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 () 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
reconsider H = G . 1 as Group by FINSEQ_1:def 8;
reconsider z = p . 1 as Element of H by ;
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 ; :: thesis: ( p . i = (z ") " & z " = lF . i )
thus p . i = (z ") " by ; :: thesis: z " = lF . i
i = 1 by ;
hence z " = lF . i by ; :: thesis: verum
end;
hence <*x*> " = <*(x ")*> by Th7; :: thesis: verum