consider Y0 being set such that
A1: for y being set holds
( y in Y0 iff ex h being Function st
( h in dom v & y in rng h ) ) and
A2: for a being set holds
( a in dom (v ** (f,N)) iff ( a in Funcs (N,Y0) & ex g being Function st
( a = g & g * f in dom v ) ) ) by Def13;
A3: dom v = Funcs (X,Y) by FUNCT_2:def 1;
A4: Y0 = Y

proof

thus Y0 c= Y :: according to XBOOLE_0:def 10 :: thesis: Y c= Y0

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Y0 or y in Y )
assume y in Y0 ; :: thesis: y in Y
then consider h being Function such that
A5: h in dom v and
A6: y in rng h by A1;
rng h c= Y by A5, FUNCT_2:92;
hence y in Y by A6; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in Y0 )
assume y in Y ; :: thesis: y in Y0
then reconsider y = y as Element of Y ;
reconsider h = X --> y as Function of X,Y ;
A7: rng h = {y} by FUNCOP_1:8;
A8: h in Funcs (X,Y) by FUNCT_2:8;
y in {y} by TARSKI:def 1;
hence y in Y0 by A3, A1, A7, A8; :: thesis: verum

end;

A9: dom (v ** (f,N)) = Funcs (N,Y)

proof

thus dom (v ** (f,N)) c= Funcs (N,Y) by A2, A4; :: according to XBOOLE_0:def 10 :: thesis: Funcs (N,Y) c= dom (v ** (f,N))
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Funcs (N,Y) or a in dom (v ** (f,N)) )
assume A10: a in Funcs (N,Y) ; :: thesis: a in dom (v ** (f,N))
then reconsider g = a as Function of N,Y by FUNCT_2:66;
g * f in Funcs (X,Y) by FUNCT_2:8;
hence a in dom (v ** (f,N)) by A3, A2, A4, A10; :: thesis: verum

end;

rng (v ** (f,N)) c= Z

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng (v ** (f,N)) or a in Z )
assume a in rng (v ** (f,N)) ; :: thesis: a in Z
then consider g being object such that
A11: g in dom (v ** (f,N)) and
A12: a = (v ** (f,N)) . g by FUNCT_1:def 3;
reconsider g = g as Element of Funcs (N,Y) by A9, A11;
reconsider gf = g * f as Element of Funcs (X,Y) by FUNCT_2:8;
a = v . gf by A11, A12, Def13;
hence a in Z ; :: thesis: verum

end;

hence v ** (f,N) is Element of Funcs ((Funcs (N,Y)),Z) by A9, FUNCT_2:def 2; :: thesis: verum