let R be Ring; :: thesis: for a, b being Element of R holds (a | R) + (b | R) = (a + b) | R
let a, b be Element of R; :: thesis: (a | R) + (b | R) = (a + b) | R
set p = (a | R) + (b | R);
set q = (a + b) | R;
A: dom ((a | R) + (b | R)) = NAT by FUNCT_2:def 1
.= dom ((a + b) | R) by FUNCT_2:def 1 ;

now :: thesis: for x being object st x in dom ((a + b) | R) holds
((a + b) | R) . x = ((a | R) + (b | R)) . x

let x be object ; :: thesis: ( x in dom ((a + b) | R) implies ((a + b) | R) . b₁ = ((a | R) + (b | R)) . b₁ )
assume x in dom ((a + b) | R) ; :: thesis: ((a + b) | R) . b₁ = ((a | R) + (b | R)) . b₁
then reconsider i = x as Element of NAT ;
B: ((a | R) + (b | R)) . i = ((a | R) . i) + ((b | R) . i) by NORMSP_1:def 2;

per cases ( i = 0 or i <> 0 ) ;

suppose S: i = 0 ; :: thesis: ((a + b) | R) . b₁ = ((a | R) + (b | R)) . b₁

hence ((a + b) | R) . x = a + b by Th28
.= ((a | R) . i) + b by S, Th28
.= ((a | R) + (b | R)) . x by B, S, Th28 ;
:: thesis: verum

end;

suppose S: i <> 0 ; :: thesis: ((a + b) | R) . b₁ = ((a | R) + (b | R)) . b₁

hence ((a + b) | R) . x = 0. R by Th28
.= ((a | R) . i) + (0. R) by S, Th28
.= ((a | R) + (b | R)) . x by B, S, Th28 ;
:: thesis: verum

end;

end;

end;

hence (a | R) + (b | R) = (a + b) | R by A, FUNCT_1:2; :: thesis: verum