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

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