set IT = n -BinaryGroup ;
hereby :: according to RLVECT_1:def 3 :: thesis:
let u, v, w be Element of (); :: thesis: (u + v) + w = u + (v + w)
reconsider u1 = u, v1 = v, w1 = w as Element of n -tuples_on BOOLEAN ;
A1: u + v = Op-XOR (u1,v1) by Def1;
A2: v + w = Op-XOR (v1,w1) by Def1;
thus (u + v) + w = Op-XOR ((Op-XOR (u1,v1)),w1) by
.= Op-XOR (u1,(Op-XOR (v1,w1))) by Th1
.= u + (v + w) by ; :: thesis: verum
end;
hereby :: according to RLVECT_1:def 4 :: thesis: ( n -BinaryGroup is right_complementable & n -BinaryGroup is Abelian & not n -BinaryGroup is empty )
let v be Element of (); :: thesis: v + (0. ()) = v
reconsider v1 = v as Element of n -tuples_on BOOLEAN ;
thus v + (0. ()) = Op-XOR (v1,()) by Def1
.= v by Th2 ; :: thesis: verum
end;
hereby :: according to ALGSTR_0:def 16 :: thesis: ( n -BinaryGroup is Abelian & not n -BinaryGroup is empty )
let v be Element of (); :: thesis:
thus v is right_complementable :: thesis: verum
proof
reconsider v1 = v as Element of n -tuples_on BOOLEAN ;
take v ; :: according to ALGSTR_0:def 11 :: thesis: v + v = 0. ()
thus v + v = Op-XOR (v1,v1) by Def1
.= 0. () by Th3 ; :: thesis: verum
end;
end;
hereby :: according to RLVECT_1:def 2 :: thesis: not n -BinaryGroup is empty
let u, v be Element of (); :: thesis: u + v = v + u
reconsider u1 = u, v1 = v as Element of n -tuples_on BOOLEAN ;
thus u + v = Op-XOR (v1,u1) by Def1
.= v + u by Def1 ; :: thesis: verum
end;
thus not n -BinaryGroup is empty ; :: thesis: verum