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
A9:
dom (v ** (f,N)) = Funcs (N,Y)
proof
thus
dom (v ** (f,N)) c= Funcs (
N,
Y)
by A2, A4;
XBOOLE_0:def 10 Funcs (N,Y) c= dom (v ** (f,N))
let a be
object ;
TARSKI:def 3 ( not a in Funcs (N,Y) or a in dom (v ** (f,N)) )
assume A10:
a in Funcs (
N,
Y)
;
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;
verum
end;
rng (v ** (f,N)) c= Z
hence
v ** (f,N) is Element of Funcs ((Funcs (N,Y)),Z)
by A9, FUNCT_2:def 2; verum