let X, Y be set ; :: thesis: for f being PartFunc of X,Y holds TotFuncs f c= Funcs (X,Y)
let f be PartFunc of X,Y; :: thesis: TotFuncs f c= Funcs (X,Y)
per cases ( ( Y = {} & X <> {} ) or Y <> {} or X = {} ) ;
suppose ( Y = {} & X <> {} ) ; :: thesis: TotFuncs f c= Funcs (X,Y)
hence TotFuncs f c= Funcs (X,Y) ; :: thesis: verum
end;
suppose A1: ( Y <> {} or X = {} ) ; :: thesis: TotFuncs f c= Funcs (X,Y)
let g be object ; :: according to TARSKI:def 3 :: thesis: ( not g in TotFuncs f or g in Funcs (X,Y) )
assume g in TotFuncs f ; :: thesis: g in Funcs (X,Y)
then g is Function of X,Y by Th81;
hence g in Funcs (X,Y) by A1, Th8; :: thesis: verum
end;
end;