let f be Function; :: thesis: for a, b, c, d being set st a <> b holds
( (f +* (a,b --> c,d)) . a = c & (f +* (a,b --> c,d)) . b = d )
let a, b, c, d be set ; :: thesis: ( a <> b implies ( (f +* (a,b --> c,d)) . a = c & (f +* (a,b --> c,d)) . b = d ) )
assume A1: a <> b ; :: thesis: ( (f +* (a,b --> c,d)) . a = c & (f +* (a,b --> c,d)) . b = d )
set g = a,b --> c,d;
A2: dom (a,b --> c,d) = {a,b} by Th65;
then a in dom (a,b --> c,d) by TARSKI:def 2;
hence (f +* (a,b --> c,d)) . a = (a,b --> c,d) . a by Th14
.= c by A1, Th66 ;
:: thesis: (f +* (a,b --> c,d)) . b = d
b in dom (a,b --> c,d) by A2, TARSKI:def 2;
hence (f +* (a,b --> c,d)) . b = (a,b --> c,d) . b by Th14
.= d by Th66 ;
:: thesis: verum