let a, b, c, d be set ; :: thesis: for f being Function st a <> b & c in dom f & d in dom f holds
f * ((a,b) --> (c,d)) = (a,b) --> ((f . c),(f . d))
let f be Function; :: thesis: ( a <> b & c in dom f & d in dom f implies f * ((a,b) --> (c,d)) = (a,b) --> ((f . c),(f . d)) )
assume that
A1: a <> b and
A2: ( c in dom f & d in dom f ) ; :: thesis: f * ((a,b) --> (c,d)) = (a,b) --> ((f . c),(f . d))
A3: dom ((a,b) --> (c,d)) = {a,b} by FUNCT_4:62;
then a in dom ((a,b) --> (c,d)) by TARSKI:def 2;
then A4: (f * ((a,b) --> (c,d))) . a = f . (((a,b) --> (c,d)) . a) by FUNCT_1:13
.= f . c by A1, FUNCT_4:63 ;
b in dom ((a,b) --> (c,d)) by A3, TARSKI:def 2;
then A5: (f * ((a,b) --> (c,d))) . b = f . (((a,b) --> (c,d)) . b) by FUNCT_1:13
.= f . d by FUNCT_4:63 ;
A6: rng ((a,b) --> (c,d)) c= {c,d} by FUNCT_4:62;
{c,d} c= dom f by A2, ZFMISC_1:32;
then dom (f * ((a,b) --> (c,d))) = {a,b} by A3, A6, RELAT_1:27, XBOOLE_1:1;
hence f * ((a,b) --> (c,d)) = (a,b) --> ((f . c),(f . d)) by A4, A5, FUNCT_4:66; :: thesis: verum