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

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

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

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

end;

suppose A1: ( 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 A1, Th11; :: thesis: verum

end;

assume A2: g in Funcs X,Y ; :: thesis: g in TotFuncs <:{} ,X,Y:>
then A3: g is Function of X,Y by Th121;
reconsider g' = g as PartFunc of X,Y by A2, Th121;
( <:{} ,X,Y:> tolerates g' & g' is total ) by A1, A3, PARTFUN1:142;
hence g in TotFuncs <:{} ,X,Y:> by PARTFUN1:def 7; :: thesis: verum

end;

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

end;

end;