let n be Ordinal; :: thesis: for R being non degenerated Ring
for a, b being Element of R holds (a | (n,R)) + (b | (n,R)) = (a + b) | (n,R)
let L be non degenerated Ring; :: thesis: for a, b being Element of L holds (a | (n,L)) + (b | (n,L)) = (a + b) | (n,L)
let a, b be Element of L; :: thesis: (a | (n,L)) + (b | (n,L)) = (a + b) | (n,L)
set p = (a + b) | (n,L);

A2: now :: thesis: for x being object st x in dom ((a + b) | (n,L)) holds
((a | (n,L)) + (b | (n,L))) . x = ((a + b) | (n,L)) . x

let x be object ; :: thesis: ( x in dom ((a + b) | (n,L)) implies ((a | (n,L)) + (b | (n,L))) . b₁ = ((a + b) | (n,L)) . b₁ )
assume x in dom ((a + b) | (n,L)) ; :: thesis: ((a | (n,L)) + (b | (n,L))) . b₁ = ((a + b) | (n,L)) . b₁
then reconsider i = x as Element of Bags n ;

per cases ( i = EmptyBag n or i <> EmptyBag n ) ;

suppose H: i = EmptyBag n ; :: thesis: ((a | (n,L)) + (b | (n,L))) . b₁ = ((a + b) | (n,L)) . b₁

thus ((a | (n,L)) + (b | (n,L))) . x = ((a | (n,L)) . i) + ((b | (n,L)) . i) by POLYNOM1:15
.= a + ((b | (n,L)) . i) by H, POLYNOM7:18
.= a + b by H, POLYNOM7:18
.= ((a + b) | (n,L)) . x by H, POLYNOM7:18 ; :: thesis: verum

end;

suppose H: i <> EmptyBag n ; :: thesis: ((a | (n,L)) + (b | (n,L))) . b₁ = ((a + b) | (n,L)) . b₁

thus ((a | (n,L)) + (b | (n,L))) . x = ((a | (n,L)) . i) + ((b | (n,L)) . i) by POLYNOM1:15
.= (0. L) + ((b | (n,L)) . i) by H, POLYNOM7:18
.= 0. L by H, POLYNOM7:18
.= ((a + b) | (n,L)) . x by H, POLYNOM7:18 ; :: thesis: verum

end;

end;

end;

dom ((a + b) | (n,L)) = Bags n by FUNCT_2:def 1;
hence (a | (n,L)) + (b | (n,L)) = (a + b) | (n,L) by A2; :: thesis: verum