defpred S₁[ object , object ] means ( ( a in f . $1 implies $2 = (f . $1) \/ {b} ) & ( not a in f . $1 implies $2 = f . $1 ) );
A1: for e being object st e in dom f holds
ex u being object st S₁[e,u]

proof

let e be object ; :: thesis: ( e in dom f implies ex u being object st S₁[e,u] )
( a in f . e or not a in f . e ) ;
hence ( e in dom f implies ex u being object st S₁[e,u] ) ; :: thesis: verum

end;

consider s being Function such that
A2: ( dom s = dom f & ( for e being object st e in dom f holds
S₁[e,s . e] ) ) from CLASSES1:sch 1(A1);
take s ; :: thesis: ( dom s = dom f & ( for x being object st x in dom f holds
( ( a in f . x implies s . x = (f . x) \/ {b} ) & ( not a in f . x implies s . x = f . x ) ) ) )
thus ( dom s = dom f & ( for x being object st x in dom f holds
( ( a in f . x implies s . x = (f . x) \/ {b} ) & ( not a in f . x implies s . x = f . x ) ) ) ) by A2; :: thesis: verum