let a, b, x, y be object ; :: thesis: for f being Function st b <> x & b <> y holds
( b in (Ext (f,x,y)) . a iff b in f . a )
let f be Function; :: thesis: ( b <> x & b <> y implies ( b in (Ext (f,x,y)) . a iff b in f . a ) )
assume A1: ( b <> x & b <> y ) ; :: thesis: ( b in (Ext (f,x,y)) . a iff b in f . a )
thus ( b in (Ext (f,x,y)) . a implies b in f . a ) :: thesis: ( b in f . a implies b in (Ext (f,x,y)) . a )

proof

assume A2: b in (Ext (f,x,y)) . a ; :: thesis: b in f . a
then a in dom (Ext (f,x,y)) by FUNCT_1:def 2;
then A3: a in dom f by Def5;

per cases ( x in f . a or not x in f . a ) ;

suppose x in f . a ; :: thesis: b in f . a

then (Ext (f,x,y)) . a = (f . a) \/ {y} by Def5, A3;
hence b in f . a by A2, A1, ZFMISC_1:136; :: thesis: verum

end;

suppose not x in f . a ; :: thesis: b in f . a

hence b in f . a by A2, A3, Def5; :: thesis: verum

end;

end;

end;

assume A4: b in f . a ; :: thesis: b in (Ext (f,x,y)) . a
then A5: a in dom f by FUNCT_1:def 2;

per cases ( x in f . a or not x in f . a ) ;

suppose x in f . a ; :: thesis: b in (Ext (f,x,y)) . a

then (Ext (f,x,y)) . a = (f . a) \/ {y} by Def5, A5;
hence b in (Ext (f,x,y)) . a by A4, XBOOLE_0:def 3; :: thesis: verum

end;

suppose not x in f . a ; :: thesis: b in (Ext (f,x,y)) . a

hence b in (Ext (f,x,y)) . a by A4, A5, Def5; :: thesis: verum

end;

end;