per cases ( u = 0. Z_2 or u = 1. Z_2 ) by BSPACE:5, BSPACE:6, XBOOLEAN:def 3;

suppose u = 0. Z_2 ; :: thesis: u + v = u 'xor' v

hence u + v = u 'xor' v by RLVECT_1:4, BSPACE:5; :: thesis: verum

end;

suppose A1: u = 1. Z_2 ; :: thesis: u + v = u 'xor' v

per cases ( v = 0. Z_2 or v = 1. Z_2 ) by BSPACE:5, BSPACE:6, XBOOLEAN:def 3;

suppose v = 0. Z_2 ; :: thesis: u + v = u 'xor' v

hence u + v = u 'xor' v by RLVECT_1:4, BSPACE:5; :: thesis: verum

end;

suppose v = 1. Z_2 ; :: thesis: u + v = u 'xor' v

hence u + v = u 'xor' v by A1, BSPACE:5, BSPACE:7, XBOOLEAN:147; :: thesis: verum

end;

end;

end;

end;