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

suppose A2: u = 0. Z_2 ; :: thesis: u * v = u '&' 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 '&' v

then u * v = (0. Z_2) * (0. Z_2)
.= 0 by BSPACE:5 ;
hence u * v = u '&' v by A2; :: thesis: verum

end;

suppose v = 1. Z_2 ; :: thesis: u * v = u '&' v

u * v = (0. Z_2) * (1. Z_2) by A2
.= 0 by BSPACE:5 ;
hence u * v = u '&' v by A2; :: thesis: verum

end;

end;

end;

suppose A3: u = 1. Z_2 ; :: thesis: u * v = u '&' v

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

suppose A4: v = 0. Z_2 ; :: thesis: u * v = u '&' v

then u * v = (1. Z_2) * (0. Z_2)
.= 0 by BSPACE:5 ;
hence u * v = u '&' v by A4; :: thesis: verum

end;

suppose v = 1. Z_2 ; :: thesis: u * v = u '&' v

hence u * v = u '&' v by A3; :: thesis: verum

end;

end;

end;

end;