let a be Element of (Z/ 2); :: thesis: a is square

per cases ( a = 0. (Z/ 2) or a = 1. (Z/ 2) ) by cz2, TARSKI:def 2;

suppose a = 0. (Z/ 2) ; :: thesis: a is square

hence a is square ; :: thesis: verum

end;

suppose a = 1. (Z/ 2) ; :: thesis: a is square

hence a is square ; :: thesis: verum

end;

end;