set Q = Trivial-multLoopStr ;
let f, g be Function of Trivial-multLoopStr,Trivial-multLoopStr; :: according to AIMLOOP:def 52 :: thesis: ( f in InnAut Trivial-multLoopStr & g in InnAut Trivial-multLoopStr implies f * g = g * f )
for x being Element of Trivial-multLoopStr holds (f * g) . x = (g * f) . x by ALGSTR_1:9;
hence ( f in InnAut Trivial-multLoopStr & g in InnAut Trivial-multLoopStr implies f * g = g * f ) by FUNCT_2:def 8; :: thesis: verum