let X, Y be set ; :: thesis: for f being PartFunc of X,Y st ( Y = {} implies X = {} ) holds
ex g being Function of X,Y st
for x being object st x in dom f holds
g . x = f . x
let f be PartFunc of X,Y; :: thesis: ( ( Y = {} implies X = {} ) implies ex g being Function of X,Y st
for x being object st x in dom f holds
g . x = f . x )
assume A1: ( Y = {} implies X = {} ) ; :: thesis: ex g being Function of X,Y st
for x being object st x in dom f holds
g . x = f . x

per cases ( Y = {} or Y <> {} ) ;

suppose Y = {} ; :: thesis: ex g being Function of X,Y st
for x being object st x in dom f holds
g . x = f . x

then reconsider g = f as Function of X,Y by A1;
take g ; :: thesis: for x being object st x in dom f holds
g . x = f . x
thus for x being object st x in dom f holds
g . x = f . x ; :: thesis: verum

end;

suppose A2: Y <> {} ; :: thesis: ex g being Function of X,Y st
for x being object st x in dom f holds
g . x = f . x

deffunc H₁( object ) -> set = f . $1;
defpred S₁[ object ] means $1 in dom f;
set y = the Element of Y;
deffunc H₂( object ) -> Element of Y = the Element of Y;
A3: for x being object st x in X holds
( ( S₁[x] implies H₁(x) in Y ) & ( not S₁[x] implies H₂(x) in Y ) ) by A2, PARTFUN1:4;
consider g being Function of X,Y such that
A4: for x being object st x in X holds
( ( S₁[x] implies g . x = H₁(x) ) & ( not S₁[x] implies g . x = H₂(x) ) ) from FUNCT_2:sch 5(A3);
take g ; :: thesis: for x being object st x in dom f holds
g . x = f . x
thus for x being object st x in dom f holds
g . x = f . x by A4; :: thesis: verum

end;

end;