let s be Real; :: thesis: (Rotate s) . (0. (TOP-REAL 2)) = 0. (TOP-REAL 2)
thus (Rotate s) . (0. (TOP-REAL 2)) = cpx2euc (Rotate ((euc2cpx (0. (TOP-REAL 2))),s)) by JORDAN24:def 3
.= 0. (TOP-REAL 2) by COMPLEX2:52, EUCLID_3:16, EUCLID_3:17 ; :: thesis: verum