set xy = <*x,y,z*>;
set G = <*G1,G2,G3*>;
A1:
dom (Carrier <*G1,G2,G3*>) = {1,2,3}
by PARTFUN1:def 2;
A2:
<*x,y,z*> . 2 = y
by FINSEQ_1:45;
A3:
<*G1,G2,G3*> . 1 = G1
by FINSEQ_1:45;
A4:
<*x,y,z*> . 3 = z
by FINSEQ_1:45;
A5:
<*G1,G2,G3*> . 3 = G3
by FINSEQ_1:45;
A6:
<*G1,G2,G3*> . 2 = G2
by FINSEQ_1:45;
A7:
<*x,y,z*> . 1 = x
by FINSEQ_1:45;
A8:
for a being object st a in {1,2,3} holds
<*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a
proof
let a be
object ;
( a in {1,2,3} implies <*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a )
assume A9:
a in {1,2,3}
;
<*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a
per cases
( a = 1 or a = 2 or a = 3 )
by A9, ENUMSET1:def 1;
suppose A10:
a = 1
;
<*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . athen
ex
R being
1-sorted st
(
R = <*G1,G2,G3*> . 1 &
(Carrier <*G1,G2,G3*>) . 1
= the
carrier of
R )
by A9, PRALG_1:def 15;
hence
<*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a
by A7, A3, A10;
verum end; suppose A11:
a = 2
;
<*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . athen
ex
R being
1-sorted st
(
R = <*G1,G2,G3*> . 2 &
(Carrier <*G1,G2,G3*>) . 2
= the
carrier of
R )
by A9, PRALG_1:def 15;
hence
<*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a
by A2, A6, A11;
verum end; suppose A12:
a = 3
;
<*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . athen
ex
R being
1-sorted st
(
R = <*G1,G2,G3*> . 3 &
(Carrier <*G1,G2,G3*>) . 3
= the
carrier of
R )
by A9, PRALG_1:def 15;
hence
<*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a
by A4, A5, A12;
verum end; end;
end;
dom <*x,y,z*> = {1,2,3}
by FINSEQ_1:89, FINSEQ_3:1;
then
<*x,y,z*> in product (Carrier <*G1,G2,G3*>)
by A1, A8, CARD_3:9;
hence
<*x,y,z*> is Element of (product <*G1,G2,G3*>)
by Def2; verum