let S1, S2 be Function; :: thesis: ( dom S1 = dom f & ( for x being object st x in dom f holds
( ( a in f . x implies S1 . x = ((f . x) \ {a}) \/ {b} ) & ( not a in f . x implies S1 . x = (f . x) \/ {a} ) ) ) & dom S2 = dom f & ( for x being object st x in dom f holds
( ( a in f . x implies S2 . x = ((f . x) \ {a}) \/ {b} ) & ( not a in f . x implies S2 . x = (f . x) \/ {a} ) ) ) implies S1 = S2 )
assume that
A3: ( dom S1 = dom f & ( for x being object st x in dom f holds
( ( a in f . x implies S1 . x = ((f . x) \ {a}) \/ {b} ) & ( not a in f . x implies S1 . x = (f . x) \/ {a} ) ) ) ) and
A4: ( dom S2 = dom f & ( for x being object st x in dom f holds
( ( a in f . x implies S2 . x = ((f . x) \ {a}) \/ {b} ) & ( not a in f . x implies S2 . x = (f . x) \/ {a} ) ) ) ) ; :: thesis: S1 = S2
for x being object st x in dom S1 holds
S1 . x = S2 . x

proof

let x be object ; :: thesis: ( x in dom S1 implies S1 . x = S2 . x )
assume A5: x in dom S1 ; :: thesis: S1 . x = S2 . x

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

suppose a in f . x ; :: thesis: S1 . x = S2 . x

then ( S1 . x = ((f . x) \ {a}) \/ {b} & ((f . x) \ {a}) \/ {b} = S2 . x ) by A3, A4, A5;
hence S1 . x = S2 . x ; :: thesis: verum

end;

suppose not a in f . x ; :: thesis: S1 . x = S2 . x

then ( S1 . x = (f . x) \/ {a} & (f . x) \/ {a} = S2 . x ) by A3, A4, A5;
hence S1 . x = S2 . x ; :: thesis: verum

end;

end;

end;

hence S1 = S2 by A3, A4; :: thesis: verum