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 set holds
( g in TotFuncs <:{} ,X,Y:> iff g in Funcs X,Y )

proof

let g be set ; :: 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 Th158;
hence g in Funcs X,Y by A2, Th11; :: 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 Th121;
A4: <:{} ,X,Y:> tolerates g9 by PARTFUN1:142;
g is Function of X,Y by A3, Th121;
hence g in TotFuncs <:{} ,X,Y:> by A2, A4, PARTFUN1:def 7; :: thesis: verum

end;

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

end;

end;