let G1, G2, G3 be Group; :: thesis: for x being Element of G1
for y being Element of G2
for z being Element of G3 holds <*x,y,z*> " = <*(x " ),(y " ),(z " )*>
let x be Element of G1; :: thesis: for y being Element of G2
for z being Element of G3 holds <*x,y,z*> " = <*(x " ),(y " ),(z " )*>
let y be Element of G2; :: thesis: for z being Element of G3 holds <*x,y,z*> " = <*(x " ),(y " ),(z " )*>
let z be Element of G3; :: thesis: <*x,y,z*> " = <*(x " ),(y " ),(z " )*>
set G = <*G1,G2,G3*>;
reconsider lF = <*x,y,z*>, p = <*(x " ),(y " ),(z " )*> as Element of product (Carrier <*G1,G2,G3*>) by Def2;
A1: ( p . 1 = x " & p . 2 = y " & p . 3 = z " & <*G1,G2,G3*> . 1 = G1 & <*G1,G2,G3*> . 2 = G2 & <*G1,G2,G3*> . 3 = G3 & lF . 1 = x & lF . 2 = y & lF . 3 = z ) by FINSEQ_1:62;
A2: p is ManySortedSet of

proof

dom p = {1,2,3} by FINSEQ_3:1, FINSEQ_3:30;
hence p is ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18; :: thesis: verum

end;

for i being set st i in {1,2,3} holds
ex H being Group ex z being Element of H st
( H = <*G1,G2,G3*> . i & p . i = z " & z = lF . i )

proof

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

per cases ( i = 1 or i = 2 or i = 3 ) by A3, ENUMSET1:def 1;

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

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

end;

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

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

end;

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

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

end;

end;

end;

hence <*x,y,z*> " = <*(x " ),(y " ),(z " )*> by A2, Th10; :: thesis: verum