let n be Nat; :: thesis: for f1, f2 being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) holds AutMt (f1 * f2) = (AutMt f2) * (AutMt f1)
let f1, f2 be additive homogeneous Function of (TOP-REAL n),(TOP-REAL n); :: thesis: AutMt (f1 * f2) = (AutMt f2) * (AutMt f1)
set A1 = AutMt f1;
set A2 = AutMt f2;
A1: ( width (AutMt f1) = n & width (AutMt f2) = n & len (AutMt f2) = n ) by MATRIX_0:24;
( n = 0 implies n = 0 ) ;
then Mx2Tran ((AutMt f2) * (AutMt f1)) = (Mx2Tran (AutMt f1)) * (Mx2Tran (AutMt f2)) by A1, MATRTOP1:32
.= f1 * (Mx2Tran (AutMt f2)) by Def6
.= f1 * f2 by Def6 ;
hence AutMt (f1 * f2) = (AutMt f2) * (AutMt f1) by Def6; :: thesis: verum