theorem
for
a,
b,
c being
Element of
F_Real for
M,
N being
Matrix of 3,
F_Real st
N = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> holds
(
((M @) * (N * M)) * (1,1)
= (((a * (M * (1,1))) * (M * (1,1))) + ((b * (M * (2,1))) * (M * (2,1)))) + ((c * (M * (3,1))) * (M * (3,1))) &
((M @) * (N * M)) * (1,2)
= (((a * (M * (1,1))) * (M * (1,2))) + ((b * (M * (2,1))) * (M * (2,2)))) + ((c * (M * (3,1))) * (M * (3,2))) &
((M @) * (N * M)) * (1,3)
= (((a * (M * (1,1))) * (M * (1,3))) + ((b * (M * (2,1))) * (M * (2,3)))) + ((c * (M * (3,1))) * (M * (3,3))) &
((M @) * (N * M)) * (2,1)
= (((a * (M * (1,2))) * (M * (1,1))) + ((b * (M * (2,2))) * (M * (2,1)))) + ((c * (M * (3,2))) * (M * (3,1))) &
((M @) * (N * M)) * (2,2)
= (((a * (M * (1,2))) * (M * (1,2))) + ((b * (M * (2,2))) * (M * (2,2)))) + ((c * (M * (3,2))) * (M * (3,2))) &
((M @) * (N * M)) * (2,3)
= (((a * (M * (1,2))) * (M * (1,3))) + ((b * (M * (2,2))) * (M * (2,3)))) + ((c * (M * (3,2))) * (M * (3,3))) &
((M @) * (N * M)) * (3,1)
= (((a * (M * (1,3))) * (M * (1,1))) + ((b * (M * (2,3))) * (M * (2,1)))) + ((c * (M * (3,3))) * (M * (3,1))) &
((M @) * (N * M)) * (3,2)
= (((a * (M * (1,3))) * (M * (1,2))) + ((b * (M * (2,3))) * (M * (2,2)))) + ((c * (M * (3,3))) * (M * (3,2))) &
((M @) * (N * M)) * (3,3)
= (((a * (M * (1,3))) * (M * (1,3))) + ((b * (M * (2,3))) * (M * (2,3)))) + ((c * (M * (3,3))) * (M * (3,3))) )