let X, Y, Z, D be set ; ( D c= Funcs ([:X,Y:],Z) implies ex F being ManySortedSet of D st
( F is currying & ( ( Y = {} implies X = {} ) implies rng F c= Funcs (X,(Funcs (Y,Z))) ) ) )
assume A1:
D c= Funcs ([:X,Y:],Z)
; ex F being ManySortedSet of D st
( F is currying & ( ( Y = {} implies X = {} ) implies rng F c= Funcs (X,(Funcs (Y,Z))) ) )
per cases
( D is empty or not D is empty )
;
suppose
D is
empty
;
ex F being ManySortedSet of D st
( F is currying & ( ( Y = {} implies X = {} ) implies rng F c= Funcs (X,(Funcs (Y,Z))) ) )then reconsider F =
{} as
ManySortedSet of
D by PARTFUN1:def 2, RELAT_1:38, RELAT_1:def 18;
take
F
;
( F is currying & ( ( Y = {} implies X = {} ) implies rng F c= Funcs (X,(Funcs (Y,Z))) ) )thus
F is
currying
;
( ( Y = {} implies X = {} ) implies rng F c= Funcs (X,(Funcs (Y,Z))) )assume
(
Y = {} implies
X = {} )
;
rng F c= Funcs (X,(Funcs (Y,Z)))thus
rng F c= Funcs (
X,
(Funcs (Y,Z)))
;
verum end; suppose
not
D is
empty
;
ex F being ManySortedSet of D st
( F is currying & ( ( Y = {} implies X = {} ) implies rng F c= Funcs (X,(Funcs (Y,Z))) ) )then reconsider E =
D as non
empty functional set by A1;
deffunc H1(
Function)
-> set =
curry $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 currying & ( ( Y = {} implies X = {} ) implies rng F1 c= Funcs (X,(Funcs (Y,Z))) ) )thus
F1 is
currying
( ( Y = {} implies X = {} ) implies rng F1 c= Funcs (X,(Funcs (Y,Z))) )assume A4:
(
Y = {} implies
X = {} )
;
rng F1 c= Funcs (X,(Funcs (Y,Z)))thus
rng F1 c= Funcs (
X,
(Funcs (Y,Z)))
verumproof
let y be
object ;
TARSKI:def 3 ( not y in rng F1 or y in Funcs (X,(Funcs (Y,Z))) )
assume
y in rng F1
;
y in Funcs (X,(Funcs (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:
y = curry d
by A2, A6;
A8:
d in Funcs (
[:X,Y:],
Z)
by A1;
per cases
( [:X,Y:] = {} or [:X,Y:] <> {} )
;
suppose A9:
[:X,Y:] = {}
;
y in Funcs (X,(Funcs (Y,Z)))then A10:
d is
Function of
{},
Z
by A8, FUNCT_2:66;
now ( X = {} implies y in Funcs (X,(Funcs (Y,Z))) )assume A11:
X = {}
;
y in Funcs (X,(Funcs (Y,Z)))then
y is
Function of
X,
(Funcs (Y,Z))
by A7, A10, FUNCT_5:42, RELSET_1:12;
hence
y in Funcs (
X,
(Funcs (Y,Z)))
by A11, FUNCT_2:8;
verum end; hence
y in Funcs (
X,
(Funcs (Y,Z)))
by A4, A9;
verum end; end;
end; end; end;