let f, g be Function; :: thesis: ( f c= g implies for x, y being set st not x in rng f holds
f c= g \ (y .--> x) )
assume A1: f c= g ; :: thesis: for x, y being set st not x in rng f holds
f c= g \ (y .--> x)
let x, y be set ; :: thesis: ( not x in rng f implies f c= g \ (y .--> x) )
assume not x in rng f ; :: thesis: f c= g \ (y .--> x)
then A2: not [y,x] in f by XTUPLE_0:def 13;
y .--> x = {[y,x]} by ZFMISC_1:29;
hence f c= g \ (y .--> x) by A2, A1, ZFMISC_1:34; :: thesis: verum