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

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

A9:
dom (v ** (f,N)) = Funcs (N,Y)
thus
Y0 c= Y
:: according to XBOOLE_0:def 10 :: thesis: Y c= 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;proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in Y0 )
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;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

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

proof

rng (v ** (f,N)) c= Z
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;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

proof

hence
v ** (f,N) is Element of Funcs ((Funcs (N,Y)),Z)
by A9, FUNCT_2:def 2; :: thesis: verum
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;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