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:65;
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:23
.= f . c by A1, FUNCT_4:66 ;
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:23
.= f . d by FUNCT_4:66 ;
A6: {c,d} c= dom f by A2, ZFMISC_1:38;
rng (a,b --> c,d) c= {c,d} by FUNCT_4:65;
then dom (f * (a,b --> c,d)) = {a,b} by A3, A6, RELAT_1:46, XBOOLE_1:1;
hence f * (a,b --> c,d) = a,b --> (f . c),(f . d) by A4, A5, FUNCT_4:69; :: thesis: verum