let a, b be Real; :: thesis: ( (a ^2) + (b ^2) = 1 implies not |[(- b),a,0]| is zero )
assume A1: (a ^2) + (b ^2) = 1 ; :: thesis: not |[(- b),a,0]| is zero
assume |[(- b),a,0]| is zero ; :: thesis: contradiction
then ( - b = 0 & a = 0 ) by EUCLID_5:4, FINSEQ_1:78;
hence contradiction by A1; :: thesis: verum