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 2;
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:66;
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:5;
hence f . x in (Carrier ((Seg n) --> R^1)) . x by A4, A1, A3, FUNCOP_1:7; :: thesis: verum

end;

hence f in product (Carrier ((Seg n) --> R^1)) by A2, A1, CARD_3:9; :: 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 3;
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:7;
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