for e1, e2, e3, f1, f2, f3 being Element of F_Real
for MABF, MABE, MACF, MBDF, MCDE, MACE, MBDE, MCDF being Matrix of 3,F_Real
for r1, r2 being Real st MABE = <*<*1,0,0*>,<*0,1,0*>,<*e1,e2,e3*>*> & MACF = <*<*1,0,0*>,<*0,0,1*>,<*f1,f2,f3*>*> & MBDF = <*<*0,1,0*>,<*1,1,1*>,<*f1,f2,f3*>*> & MCDE = <*<*0,0,1*>,<*1,1,1*>,<*e1,e2,e3*>*> & MABF = <*<*1,0,0*>,<*0,1,0*>,<*f1,f2,f3*>*> & MACE = <*<*1,0,0*>,<*0,0,1*>,<*e1,e2,e3*>*> & MBDE = <*<*0,1,0*>,<*1,1,1*>,<*e1,e2,e3*>*> & MCDF = <*<*0,0,1*>,<*1,1,1*>,<*f1,f2,f3*>*> & ( r1 <> 0 or r2 <> 0 ) & ((r1 * e1) * e2) + ((r2 * e1) * e3) = ((r1 + r2) * e2) * e3 & ((r1 * f1) * f2) + ((r2 * f1) * f3) = ((r1 + r2) * f2) * f3 holds
(((Det MABE) * (Det MACF)) * (Det MBDF)) * (Det MCDE) = (((Det MABF) * (Det MACE)) * (Det MBDE)) * (Det MCDF)