let X, Y, Z, D be set ; ( D c= Funcs (X,(Funcs (Y,Z))) implies ex F being ManySortedSet of D st
( F is uncurrying & rng F c= Funcs ([:X,Y:],Z) ) )
assume A1:
D c= Funcs (X,(Funcs (Y,Z)))
; ex F being ManySortedSet of D st
( F is uncurrying & rng F c= Funcs ([:X,Y:],Z) )
per cases
( D is empty or not D is empty )
;
suppose
not
D is
empty
;
ex F being ManySortedSet of D st
( F is uncurrying & rng F c= Funcs ([:X,Y:],Z) )then reconsider E =
D as non
empty functional set by A1;
deffunc H1(
Function)
-> set =
uncurry $1;
consider F being
ManySortedSet of
E such that A2:
for
d being
Element of
E holds
F . d = H1(
d)
from PBOOLE:sch 5();
reconsider F1 =
F as
ManySortedSet of
D ;
take
F1
;
( F1 is uncurrying & rng F1 c= Funcs ([:X,Y:],Z) )thus
F1 is
uncurrying
rng F1 c= Funcs ([:X,Y:],Z)thus
rng F1 c= Funcs (
[:X,Y:],
Z)
verumproof
let y be
object ;
TARSKI:def 3 ( not y in rng F1 or y in Funcs ([:X,Y:],Z) )
assume
y in rng F1
;
y in Funcs ([:X,Y:],Z)
then consider x being
object such that A5:
x in dom F1
and A6:
y = F1 . x
by FUNCT_1:def 3;
reconsider d =
x as
Element of
E by A5;
A7:
d in Funcs (
X,
(Funcs (Y,Z)))
by A1;
y = uncurry d
by A2, A6;
hence
y in Funcs (
[:X,Y:],
Z)
by A7, FUNCT_6:11;
verum
end; end; end;