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 set ; :: 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:169;
hence y in Y by A6; :: thesis: verum

end;

let y be set ; :: 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:14;
A8: h in Funcs X,Y by FUNCT_2:11;
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 :: according to XBOOLE_0:def 10 :: thesis: Funcs N,Y c= dom (v ** f,N)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in dom (v ** f,N) or a in Funcs N,Y )
thus ( not a in dom (v ** f,N) or a in Funcs N,Y ) by A2, A4; :: thesis: verum

end;

let a be set ; :: 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:121;
g * f in Funcs X,Y by FUNCT_2:11;
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 set ; :: 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 set such that
A11: g in dom (v ** f,N) and
A12: a = (v ** f,N) . g by FUNCT_1:def 5;
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:11;
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