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