:: deftheorem Def6 defines AutMt MATRTOP3:def 6 :
for n being Nat
for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n)
for b₃ being Matrix of n,F_Real holds
( b₃ = AutMt f iff f = Mx2Tran b₃ );