deffunc H₁( object ) -> Element of Funcs (L1,L2) = the Element of Funcs (L1,L2);
consider f being Function such that
A: ( dom f = NAT & ( for x being object st x in NAT holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
reconsider f = f as sequence by A, FIELD_12:def 2;
take f ; :: thesis: f is Funcs (L1,L2) -valued

now :: thesis: for x being object st x in rng f holds
x in Funcs (L1,L2)

let x be object ; :: thesis: ( x in rng f implies x in Funcs (L1,L2) )
assume x in rng f ; :: thesis: x in Funcs (L1,L2)
then consider o being object such that
B: ( o in dom f & f . o = x ) by FUNCT_1:def 3;
x is Element of Funcs (L1,L2) by A, B;
hence x in Funcs (L1,L2) ; :: thesis: verum

end;

then rng f c= Funcs (L1,L2) ;
hence f is Funcs (L1,L2) -valued by RELAT_1:def 19; :: thesis: verum