let n be Nat; :: thesis: Funcs (Seg n),REAL = product (Carrier ((Seg n) --> R^1 ))
set J = (Seg n) --> R^1 ;
set C = Carrier ((Seg n) --> R^1 );
A1: dom (Carrier ((Seg n) --> R^1 )) = Seg n by PARTFUN1:def 4;
thus Funcs (Seg n),REAL c= product (Carrier ((Seg n) --> R^1 )) :: according to XBOOLE_0:def 10 :: thesis: product (Carrier ((Seg n) --> R^1 )) c= Funcs (Seg n),REAL

proof

let f be set ; :: according to TARSKI:def 3 :: thesis: ( not f in Funcs (Seg n),REAL or f in product (Carrier ((Seg n) --> R^1 )) )
assume f in Funcs (Seg n),REAL ; :: thesis: f in product (Carrier ((Seg n) --> R^1 ))
then reconsider f = f as Function of (Seg n),REAL by FUNCT_2:121;
A2: dom f = Seg n by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in dom (Carrier ((Seg n) --> R^1 )) implies f . x in (Carrier ((Seg n) --> R^1 )) . x )
assume A3: x in dom (Carrier ((Seg n) --> R^1 )) ; :: thesis: f . x in (Carrier ((Seg n) --> R^1 )) . x
then A4: ex R being 1-sorted st
( R = ((Seg n) --> R^1 ) . x & (Carrier ((Seg n) --> R^1 )) . x = the carrier of R ) by A1, PRALG_1:def 13;
f . x in REAL by A1, A3, FUNCT_2:7;
hence f . x in (Carrier ((Seg n) --> R^1 )) . x by A4, A1, A3, FUNCOP_1:13; :: thesis: verum

end;

hence f in product (Carrier ((Seg n) --> R^1 )) by A2, A1, CARD_3:18; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in product (Carrier ((Seg n) --> R^1 )) or x in Funcs (Seg n),REAL )
assume x in product (Carrier ((Seg n) --> R^1 )) ; :: thesis: x in Funcs (Seg n),REAL
then consider g being Function such that
A5: x = g and
A6: dom g = dom (Carrier ((Seg n) --> R^1 )) and
A7: for y being set st y in dom (Carrier ((Seg n) --> R^1 )) holds
g . y in (Carrier ((Seg n) --> R^1 )) . y by CARD_3:def 5;
rng g c= REAL

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng g or z in REAL )
assume z in rng g ; :: thesis: z in REAL
then consider a being set such that
A8: a in dom g and
A9: g . a = z by FUNCT_1:def 5;
A10: ex R being 1-sorted st
( R = ((Seg n) --> R^1 ) . a & (Carrier ((Seg n) --> R^1 )) . a = the carrier of R ) by A1, A6, A8, PRALG_1:def 13;
((Seg n) --> R^1 ) . a = R^1 by A1, A6, A8, FUNCOP_1:13;
hence z in REAL by A6, A7, A8, A9, A10; :: thesis: verum

end;

hence x in Funcs (Seg n),REAL by A1, A5, A6, FUNCT_2:def 2; :: thesis: verum