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

A1: <*G1,G2,G3*> . 2 = G2 by FINSEQ_1:45;

A2: <*G1,G2,G3*> . 3 = G3 by FINSEQ_1:45;

reconsider lF = <*x,y,z*>, p = <*(x "),(y "),(z ")*> as Element of product (Carrier <*G1,G2,G3*>) by Def2;

A3: p . 1 = x " by FINSEQ_1:45;

A4: p . 3 = z " by FINSEQ_1:45;

A5: p . 2 = y " by FINSEQ_1:45;

A6: <*G1,G2,G3*> . 1 = G1 by FINSEQ_1:45;

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 )

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

A1: <*G1,G2,G3*> . 2 = G2 by FINSEQ_1:45;

A2: <*G1,G2,G3*> . 3 = G3 by FINSEQ_1:45;

reconsider lF = <*x,y,z*>, p = <*(x "),(y "),(z ")*> as Element of product (Carrier <*G1,G2,G3*>) by Def2;

A3: p . 1 = x " by FINSEQ_1:45;

A4: p . 3 = z " by FINSEQ_1:45;

A5: p . 2 = y " by FINSEQ_1:45;

A6: <*G1,G2,G3*> . 1 = G1 by FINSEQ_1:45;

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

hence
<*x,y,z*> " = <*(x "),(y "),(z ")*>
by Th7; :: thesis: verum
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 A7: 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 )

end;( H = <*G1,G2,G3*> . i & p . i = z " & z = lF . i ) )

assume A7: 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 A7, ENUMSET1:def 1;

end;

suppose A8:
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 )

( H = <*G1,G2,G3*> . i & p . i = z " & z = lF . i )

reconsider H = <*G1,G2,G3*> . 1 as Group by FINSEQ_1:45;

reconsider z = p . 1 as Element of H by A3, FINSEQ_1:45;

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 A8; :: thesis: ( p . i = (z ") " & z " = lF . i )

thus p . i = (z ") " by A8; :: thesis: z " = lF . i

thus z " = lF . i by A3, A6, A8, FINSEQ_1:45; :: thesis: verum

end;reconsider z = p . 1 as Element of H by A3, FINSEQ_1:45;

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 A8; :: thesis: ( p . i = (z ") " & z " = lF . i )

thus p . i = (z ") " by A8; :: thesis: z " = lF . i

thus z " = lF . i by A3, A6, A8, FINSEQ_1:45; :: thesis: verum

suppose A9:
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 )

( H = <*G1,G2,G3*> . i & p . i = z " & z = lF . i )

reconsider H = <*G1,G2,G3*> . 2 as Group by FINSEQ_1:45;

reconsider z = p . 2 as Element of H by A5, FINSEQ_1:45;

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 A9; :: thesis: ( p . i = (z ") " & z " = lF . i )

thus p . i = (z ") " by A9; :: thesis: z " = lF . i

thus z " = lF . i by A5, A1, A9, FINSEQ_1:45; :: thesis: verum

end;reconsider z = p . 2 as Element of H by A5, FINSEQ_1:45;

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 A9; :: thesis: ( p . i = (z ") " & z " = lF . i )

thus p . i = (z ") " by A9; :: thesis: z " = lF . i

thus z " = lF . i by A5, A1, A9, FINSEQ_1:45; :: thesis: verum

suppose A10:
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 )

( H = <*G1,G2,G3*> . i & p . i = z " & z = lF . i )

reconsider H = <*G1,G2,G3*> . 3 as Group by FINSEQ_1:45;

reconsider z = p . 3 as Element of H by A4, FINSEQ_1:45;

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 A10; :: thesis: ( p . i = (z ") " & z " = lF . i )

thus p . i = (z ") " by A10; :: thesis: z " = lF . i

thus z " = lF . i by A4, A2, A10, FINSEQ_1:45; :: thesis: verum

end;reconsider z = p . 3 as Element of H by A4, FINSEQ_1:45;

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 A10; :: thesis: ( p . i = (z ") " & z " = lF . i )

thus p . i = (z ") " by A10; :: thesis: z " = lF . i

thus z " = lF . i by A4, A2, A10, FINSEQ_1:45; :: thesis: verum