let x, y, z be object ; :: thesis: for f being Function st z in dom f holds
Ext ({(f . z)},x,y) = {((Ext (f,x,y)) . z)}
let f be Function; :: thesis: ( z in dom f implies Ext ({(f . z)},x,y) = {((Ext (f,x,y)) . z)} )
assume A1: z in dom f ; :: thesis: Ext ({(f . z)},x,y) = {((Ext (f,x,y)) . z)}

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

suppose x in f . z ; :: thesis: Ext ({(f . z)},x,y) = {((Ext (f,x,y)) . z)}

then ( Ext ({(f . z)},x,y) = {((f . z) \/ {y})} & (Ext (f,x,y)) . z = (f . z) \/ {y} ) by A1, Def5, Th29;
hence Ext ({(f . z)},x,y) = {((Ext (f,x,y)) . z)} ; :: thesis: verum

end;

suppose not x in f . z ; :: thesis: Ext ({(f . z)},x,y) = {((Ext (f,x,y)) . z)}

then ( Ext ({(f . z)},x,y) = {(f . z)} & (Ext (f,x,y)) . z = f . z ) by A1, Def5, Th30;
hence Ext ({(f . z)},x,y) = {((Ext (f,x,y)) . z)} ; :: thesis: verum

end;

end;