let x1, x2, y1, y2 be set ; :: thesis: for f being Function holds
( ( x1 = x2 implies (f +* (x1 .--> y1)) +* (x2 .--> y2) = f +* (x2 .--> y2) ) & ( x1 <> x2 implies (f +* (x1 .--> y1)) +* (x2 .--> y2) = (f +* (x2 .--> y2)) +* (x1 .--> y1) ) )
let f be Function; :: thesis: ( ( x1 = x2 implies (f +* (x1 .--> y1)) +* (x2 .--> y2) = f +* (x2 .--> y2) ) & ( x1 <> x2 implies (f +* (x1 .--> y1)) +* (x2 .--> y2) = (f +* (x2 .--> y2)) +* (x1 .--> y1) ) )
set f1 = x1 .--> y1;
set f2 = x2 .--> y2;
set LH = (f +* (x1 .--> y1)) +* (x2 .--> y2);
hereby :: thesis: ( x1 <> x2 implies (f +* (x1 .--> y1)) +* (x2 .--> y2) = (f +* (x2 .--> y2)) +* (x1 .--> y1) )
assume x1 = x2 ; :: thesis: (f +* (x1 .--> y1)) +* (x2 .--> y2) = f +* (x2 .--> y2)
then {x1} = dom (x2 .--> y2) ;
then dom (x1 .--> y1) = dom (x2 .--> y2) ;
then (x1 .--> y1) +* (x2 .--> y2) = x2 .--> y2 by FUNCT_4:19;
hence (f +* (x1 .--> y1)) +* (x2 .--> y2) = f +* (x2 .--> y2) by FUNCT_4:14; :: thesis: verum
end;
assume x1 <> x2 ; :: thesis: (f +* (x1 .--> y1)) +* (x2 .--> y2) = (f +* (x2 .--> y2)) +* (x1 .--> y1)
then {x1} misses {x2} by ZFMISC_1:11;
then x1 .--> y1 tolerates x2 .--> y2 by FUNCOP_1:87;
then f +* ((x1 .--> y1) +* (x2 .--> y2)) = f +* ((x2 .--> y2) +* (x1 .--> y1)) by FUNCT_4:34
.= (f +* (x2 .--> y2)) +* (x1 .--> y1) by FUNCT_4:14 ;
hence (f +* (x1 .--> y1)) +* (x2 .--> y2) = (f +* (x2 .--> y2)) +* (x1 .--> y1) by FUNCT_4:14; :: thesis: verum