let X, Y be set ; :: thesis: for f, g being PartFunc of , st g c= f holds
TotFuncs f c= TotFuncs g
let f, g be PartFunc of ,; :: thesis: ( g c= f implies TotFuncs f c= TotFuncs g )
assume A1: g c= f ; :: thesis: TotFuncs f c= TotFuncs g
let h be set ; :: according to TARSKI:def 3 :: thesis: ( not h in TotFuncs f or h in TotFuncs g )
assume A2: h in TotFuncs f ; :: thesis: h in TotFuncs g
then reconsider h' = h as PartFunc of , by PARTFUN1:168;
A3: h' is total by A2, PARTFUN1:169;
g tolerates h' by A1, A2, PARTFUN1:140, PARTFUN1:171;
hence h in TotFuncs g by A3, PARTFUN1:def 7; :: thesis: verum