theorem :: SIN_COS:29

for th being Real holds
( ((cos th) ^2) + ((sin th) ^2) = 1 & ((cos th) * (cos th)) + ((sin th) * (sin th)) = 1 ) by Th28;