A8: product <*REAL*> c= REAL 1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in product <*REAL*> or x in REAL 1 )
assume x in product <*REAL*> ; :: thesis: x in REAL 1
then consider g being Function such that
A1: x = g and
A2: dom g = dom <*REAL*> and
A3: for j being object st j in dom <*REAL*> holds
g . j in <*REAL*> . j by CARD_3:def 5;
A4: dom g = Seg 1 by A2, FINSEQ_1:def 8;
rng g c= REAL

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in rng g or u in REAL )
assume u in rng g ; :: thesis: u in REAL
then consider t being object such that
A5: t in dom g and
A6: u = g . t by FUNCT_1:def 3;
t in {1} by A5, FINSEQ_1:2, A2, FINSEQ_1:def 8;
then A7: ( t = 1 & 1 in Seg 1 ) by FINSEQ_1:2, TARSKI:def 1;
( u = g . 1 & 1 in dom <*REAL*> ) by A6, A7, FINSEQ_1:def 8;
then g . 1 in <*REAL*> . 1 by A3;
hence u in REAL by A7, A6; :: thesis: verum

end;

then x in Funcs ((Seg 1),REAL) by A1, FUNCT_2:def 2, A4;
then x in 1 -tuples_on REAL by FINSEQ_2:93;
hence x in REAL 1 by EUCLID:def 1; :: thesis: verum

end;

REAL 1 c= product <*REAL*>

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in REAL 1 or x in product <*REAL*> )
assume A9: x in REAL 1 ; :: thesis: x in product <*REAL*>
then x in 1 -tuples_on REAL by EUCLID:def 1;
then A10: x in Funcs ((Seg 1),REAL) by FINSEQ_2:93;
reconsider g = x as Function by A9;

now :: thesis: ( dom g = dom <*REAL*> & ( for j being object st j in dom <*REAL*> holds
g . j in <*REAL*> . j ) & ( for j being object st j in dom <*REAL*> holds
g . j in <*REAL*> . j ) )

consider h being Function such that
A11: h = g and
A12: dom h = Seg 1 and
A13: rng h c= REAL by A10, FUNCT_2:def 2;
thus dom g = dom <*REAL*> by A11, A12, FINSEQ_1:def 8; :: thesis: ( ( for j being object st j in dom <*REAL*> holds
g . j in <*REAL*> . j ) & ( for j being object st j in dom <*REAL*> holds
g . j in <*REAL*> . j ) )

hereby :: thesis: for j being object st j in dom <*REAL*> holds
g . j in <*REAL*> . j

let j be object ; :: thesis: ( j in dom <*REAL*> implies g . j in <*REAL*> . j )
assume A14: j in dom <*REAL*> ; :: thesis: g . j in <*REAL*> . j
then A15: j in Seg 1 by FINSEQ_1:def 8;
j in {1} by FINSEQ_1:2, A14, FINSEQ_1:def 8;
then A16: j = 1 by TARSKI:def 1;
g . j in REAL by A11, A13, A12, A15, FUNCT_1:3;
hence g . j in <*REAL*> . j by A16; :: thesis: verum

end;

hence for j being object st j in dom <*REAL*> holds
g . j in <*REAL*> . j ; :: thesis: verum

end;

hence x in product <*REAL*> by CARD_3:def 5; :: thesis: verum

end;

hence product <*REAL*> = REAL 1 by A8; :: thesis: verum