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

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