set IT = n -BinaryGroup ;

hereby :: according to RLVECT_1:def 3 :: thesis: ( n -BinaryGroup is right_zeroed & n -BinaryGroup is right_complementable & n -BinaryGroup is Abelian & not n -BinaryGroup is empty )

let u, v, w be Element of (n -BinaryGroup); :: 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 A1, Def1

.= Op-XOR (u1,(Op-XOR (v1,w1))) by Th1

.= u + (v + w) by A2, Def1 ; :: thesis: verum

end;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 A1, Def1

.= Op-XOR (u1,(Op-XOR (v1,w1))) by Th1

.= u + (v + w) by A2, Def1 ; :: thesis: verum

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 (n -BinaryGroup); :: thesis: v + (0. (n -BinaryGroup)) = v

reconsider v1 = v as Element of n -tuples_on BOOLEAN ;

thus v + (0. (n -BinaryGroup)) = Op-XOR (v1,(ZeroB n)) by Def1

.= v by Th2 ; :: thesis: verum

end;reconsider v1 = v as Element of n -tuples_on BOOLEAN ;

thus v + (0. (n -BinaryGroup)) = Op-XOR (v1,(ZeroB n)) by Def1

.= v by Th2 ; :: thesis: verum

hereby :: according to ALGSTR_0:def 16 :: thesis: ( n -BinaryGroup is Abelian & not n -BinaryGroup is empty )

let v be Element of (n -BinaryGroup); :: thesis: v is right_complementable

thus v is right_complementable :: thesis: verum

end;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. (n -BinaryGroup)

thus v + v = Op-XOR (v1,v1) by Def1

.= 0. (n -BinaryGroup) by Th3 ; :: thesis: verum

end;take v ; :: according to ALGSTR_0:def 11 :: thesis: v + v = 0. (n -BinaryGroup)

thus v + v = Op-XOR (v1,v1) by Def1

.= 0. (n -BinaryGroup) by Th3 ; :: thesis: verum

hereby :: according to RLVECT_1:def 2 :: thesis: not n -BinaryGroup is empty

thus
not n -BinaryGroup is empty
; :: thesis: verumlet u, v be Element of (n -BinaryGroup); :: 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;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