let G1, G2 be Group; :: thesis: for x being Element of G1
for y being Element of G2 holds <*x,y*> " = <*(x " ),(y " )*>
let x be Element of G1; :: thesis: for y being Element of G2 holds <*x,y*> " = <*(x " ),(y " )*>
let y be Element of G2; :: thesis: <*x,y*> " = <*(x " ),(y " )*>
set G = <*G1,G2*>;
A1: <*G1,G2*> . 2 = G2 by FINSEQ_1:61;
reconsider lF = <*x,y*>, p = <*(x " ),(y " )*> as Element of product (Carrier <*G1,G2*>) by Def2;
A2: p . 1 = x " by FINSEQ_1:61;
A3: p . 2 = y " by FINSEQ_1:61;
A4: <*G1,G2*> . 1 = G1 by FINSEQ_1:61;
A5: for i being set st i in {1,2} holds
ex H being Group ex z being Element of H st
( H = <*G1,G2*> . i & p . i = z " & z = lF . i )

proof

let i be set ; :: thesis: ( i in {1,2} implies ex H being Group ex z being Element of H st
( H = <*G1,G2*> . i & p . i = z " & z = lF . i ) )
assume A6: i in {1,2} ; :: thesis: ex H being Group ex z being Element of H st
( H = <*G1,G2*> . i & p . i = z " & z = lF . i )

per cases ( i = 1 or i = 2 ) by A6, TARSKI:def 2;

suppose A7: i = 1 ; :: thesis: ex H being Group ex z being Element of H st
( H = <*G1,G2*> . i & p . i = z " & z = lF . i )

reconsider H = <*G1,G2*> . 1 as Group by FINSEQ_1:61;
reconsider z = p . 1 as Element of H by A2, FINSEQ_1:61;
take H ; :: thesis: ex z being Element of H st
( H = <*G1,G2*> . i & p . i = z " & z = lF . i )
take z " ; :: thesis: ( H = <*G1,G2*> . i & p . i = (z " ) " & z " = lF . i )
thus H = <*G1,G2*> . i by A7; :: thesis: ( p . i = (z " ) " & z " = lF . i )
thus p . i = (z " ) " by A7; :: thesis: z " = lF . i
thus z " = lF . i by A2, A4, A7, FINSEQ_1:61; :: thesis: verum

end;

suppose A8: i = 2 ; :: thesis: ex H being Group ex z being Element of H st
( H = <*G1,G2*> . i & p . i = z " & z = lF . i )

reconsider H = <*G1,G2*> . 2 as Group by FINSEQ_1:61;
reconsider z = p . 2 as Element of H by A3, FINSEQ_1:61;
take H ; :: thesis: ex z being Element of H st
( H = <*G1,G2*> . i & p . i = z " & z = lF . i )
take z " ; :: thesis: ( H = <*G1,G2*> . i & p . i = (z " ) " & z " = lF . i )
thus H = <*G1,G2*> . i by A8; :: thesis: ( p . i = (z " ) " & z " = lF . i )
thus p . i = (z " ) " by A8; :: thesis: z " = lF . i
thus z " = lF . i by A3, A1, A8, FINSEQ_1:61; :: thesis: verum

end;

end;

end;

dom p = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
then p is ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18;
hence <*x,y*> " = <*(x " ),(y " )*> by A5, Th10; :: thesis: verum