let f1, f2 be Function; :: thesis: ( dom f1 = bool (rng f) & ( for Y being set st Y c= rng f holds
f1 . Y = f " Y ) & dom f2 = bool (rng f) & ( for Y being set st Y c= rng f holds
f2 . Y = f " Y ) implies f1 = f2 )
assume that
A6: dom f1 = bool (rng f) and
A7: for Y being set st Y c= rng f holds
f1 . Y = f " Y and
A8: dom f2 = bool (rng f) and
A9: for Y being set st Y c= rng f holds
f2 . Y = f " Y ; :: thesis: f1 = f2
for y being object st y in bool (rng f) holds
f1 . y = f2 . y

proof

let y be object ; :: thesis: ( y in bool (rng f) implies f1 . y = f2 . y )
assume A10: y in bool (rng f) ; :: thesis: f1 . y = f2 . y
reconsider y = y as set by TARSKI:1;
f1 . y = f " y by A7, A10;
hence f1 . y = f2 . y by A9, A10; :: thesis: verum

end;

hence f1 = f2 by A6, A8; :: thesis: verum