set K = unionField (S,f,E);

hereby :: according to RLVECT_1:def 2 :: thesis: ( unionField (S,f,E) is add-associative & unionField (S,f,E) is right_zeroed & unionField (S,f,E) is right_complementable )

let x, y be Element of (unionField (S,f,E)); :: thesis: x + y = y + x
reconsider a = x, b = y as Element of unionCarrier (S,f,E) by duf;
consider p being Element of S, xi, yi being Element of (p `1) such that
A: ( xi = a & yi = b & (unionAdd (S,f,E)) . (a,b) = xi + yi ) by dua;
thus x + y = xi + yi by A, lem4a
.= y + x by A, lem4a ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 3 :: thesis: ( unionField (S,f,E) is right_zeroed & unionField (S,f,E) is right_complementable )

let x, y, z be Element of (unionField (S,f,E)); :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)
reconsider a = x, b = y, c = z, ab = x + y as Element of unionCarrier (S,f,E) by duf;
consider p being Element of S, xi, yi being Element of (p `1) such that
A: ( xi = a & yi = b & (unionAdd (S,f,E)) . (a,b) = xi + yi ) by dua;
consider q being Element of S, xj, zj being Element of (q `1) such that
B: ( xj = ab & zj = c & (unionAdd (S,f,E)) . (ab,c) = xj + zj ) by dua;

per cases ( q <= p or p <= q ) by dasc;

suppose q <= p ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

then reconsider zi = zj as Element of (p `1) by lem1a;
C: yi + zi = y + z by A, B, lem4a;
x + y = xi + yi by A, lem4a;
hence (x + y) + z = (xi + yi) + zi by B, lem4a
.= xi + (yi + zi) by RLVECT_1:def 3
.= x + (y + z) by A, C, lem4a ;
:: thesis: verum

end;

suppose p <= q ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

then reconsider xj = xi, yj = yi as Element of (q `1) by lem1a;
C: yj + zj = y + z by A, B, lem4a;
x + y = xj + yj by A, lem4a;
hence (x + y) + z = (xj + yj) + zj by B, lem4a
.= xj + (yj + zj) by RLVECT_1:def 3
.= x + (y + z) by A, C, lem4a ;
:: thesis: verum

end;

end;

end;

hereby :: according to RLVECT_1:def 4 :: thesis: unionField (S,f,E) is right_complementable

let x be Element of (unionField (S,f,E)); :: thesis: x + (0. (unionField (S,f,E))) = x
x is Element of unionCarrier (S,f,E) by duf;
then consider Y being set such that
A: ( x in Y & Y in { the carrier of (p `1) where p is Element of S : verum } ) by TARSKI:def 4;
consider p being Element of S such that
B: Y = the carrier of (p `1) by A;
reconsider a = x as Element of (p `1) by A, B;
0. (unionField (S,f,E)) = 0. (p `1) by lem5a;
hence x + (0. (unionField (S,f,E))) = a + (0. (p `1)) by lem4a
.= x ;
:: thesis: verum

end;

let x be Element of (unionField (S,f,E)); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
x is Element of unionCarrier (S,f,E) by duf;
then consider Y being set such that
A: ( x in Y & Y in { the carrier of (p `1) where p is Element of S : verum } ) by TARSKI:def 4;
consider p being Element of S such that
B: Y = the carrier of (p `1) by A;
reconsider a = x as Element of (p `1) by A, B;
the carrier of (p `1) in { the carrier of (p `1) where p is Element of S : verum } ;
then - a in unionCarrier (S,f,E) by TARSKI:def 4;
then reconsider y = - a as Element of (unionField (S,f,E)) by duf;
take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. (unionField (S,f,E))
thus x + y = a + (- a) by lem4a
.= 0. (p `1) by RLVECT_1:5
.= 0. (unionField (S,f,E)) by lem5a ; :: thesis: verum