let n be Nat; :: thesis: for f, g being Function of (TOP-REAL n),(TOP-REAL n) st f is rotation & g is rotation holds
f * g is rotation
set TR = TOP-REAL n;
let f, g be Function of (TOP-REAL n),(TOP-REAL n); :: thesis: ( f is rotation & g is rotation implies f * g is rotation )
assume that
A1: f is rotation and
A2: g is rotation ; :: thesis: f * g is rotation
let p be Point of (TOP-REAL n); :: according to MATRTOP3:def 4 :: thesis: |.p.| = |.((f * g) . p).|
dom (f * g) = the carrier of (TOP-REAL n) by FUNCT_2:52;
hence |.((f * g) . p).| = |.(f . (g . p)).| by FUNCT_1:12
.= |.(g . p).| by A1
.= |.p.| by A2 ;
:: thesis: verum