let X, Y be set ; TotFuncs <:{},X,Y:> = Funcs (X,Y)
per cases
not ( not ( Y = {} & X <> {} ) & Y = {} & not X = {} )
;
suppose A2:
(
Y = {} implies
X = {} )
;
TotFuncs <:{},X,Y:> = Funcs (X,Y)
for
g being
object holds
(
g in TotFuncs <:{},X,Y:> iff
g in Funcs (
X,
Y) )
proof
let g be
object ;
( g in TotFuncs <:{},X,Y:> iff g in Funcs (X,Y) )
thus
(
g in TotFuncs <:{},X,Y:> implies
g in Funcs (
X,
Y) )
( g in Funcs (X,Y) implies g in TotFuncs <:{},X,Y:> )
assume A3:
g in Funcs (
X,
Y)
;
g in TotFuncs <:{},X,Y:>
then reconsider g9 =
g as
PartFunc of
X,
Y by Th65;
A4:
<:{},X,Y:> tolerates g9
by PARTFUN1:60;
g is
Function of
X,
Y
by A3, Th65;
hence
g in TotFuncs <:{},X,Y:>
by A2, A4, PARTFUN1:def 5;
verum
end; hence
TotFuncs <:{},X,Y:> = Funcs (
X,
Y)
by TARSKI:2;
verum end; end;