let X, Y be set ; :: thesis: TotFuncs <:{},X,Y:> = Funcs (X,Y)

per cases not ( not ( Y = {} & X <> {} ) & Y = {} & not X = {} ) ;

suppose A1: ( Y = {} & X <> {} ) ; :: thesis: TotFuncs <:{},X,Y:> = Funcs (X,Y)

then TotFuncs <:{},X,Y:> = {} ;
hence TotFuncs <:{},X,Y:> = Funcs (X,Y) by A1; :: thesis: verum

end;

suppose A2: ( Y = {} implies X = {} ) ; :: thesis: 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 ; :: thesis: ( g in TotFuncs <:{},X,Y:> iff g in Funcs (X,Y) )
thus ( g in TotFuncs <:{},X,Y:> implies g in Funcs (X,Y) ) :: thesis: ( g in Funcs (X,Y) implies g in TotFuncs <:{},X,Y:> )

proof

assume g in TotFuncs <:{},X,Y:> ; :: thesis: g in Funcs (X,Y)
then g is Function of X,Y by Th81;
hence g in Funcs (X,Y) by A2, Th8; :: thesis: verum

end;

assume A3: g in Funcs (X,Y) ; :: thesis: 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; :: thesis: verum

end;

hence TotFuncs <:{},X,Y:> = Funcs (X,Y) by TARSKI:2; :: thesis: verum

end;

end;