let A be Matrix of 3,REAL; :: thesis: Det A = (((((((A * (1,1)) * (A * (2,2))) * (A * (3,3))) - (((A * (1,3)) * (A * (2,2))) * (A * (3,1)))) - (((A * (1,1)) * (A * (2,3))) * (A * (3,2)))) + (((A * (1,2)) * (A * (2,3))) * (A * (3,1)))) - (((A * (1,2)) * (A * (2,1))) * (A * (3,3)))) + (((A * (1,3)) * (A * (2,1))) * (A * (3,2)))
reconsider N = MXR2MXF A as Matrix of 3,F_Real ;
reconsider N2 = <*<*(N * (1,1)),(N * (1,2)),(N * (1,3))*>,<*(N * (2,1)),(N * (2,2)),(N * (2,3))*>,<*(N * (3,1)),(N * (3,2)),(N * (3,3))*>*> as Matrix of 3,F_Real by Th35;
Det A = Det N2 by Th37
.= (((((((N * (1,1)) * (N * (2,2))) * (N * (3,3))) - (((N * (1,3)) * (N * (2,2))) * (N * (3,1)))) - (((N * (1,1)) * (N * (2,3))) * (N * (3,2)))) + (((N * (1,2)) * (N * (2,3))) * (N * (3,1)))) - (((N * (1,2)) * (N * (2,1))) * (N * (3,3)))) + (((N * (1,3)) * (N * (2,1))) * (N * (3,2))) by MATRIX_9:46 ;
hence Det A = (((((((A * (1,1)) * (A * (2,2))) * (A * (3,3))) - (((A * (1,3)) * (A * (2,2))) * (A * (3,1)))) - (((A * (1,1)) * (A * (2,3))) * (A * (3,2)))) + (((A * (1,2)) * (A * (2,3))) * (A * (3,1)))) - (((A * (1,2)) * (A * (2,1))) * (A * (3,3)))) + (((A * (1,3)) * (A * (2,1))) * (A * (3,2))) ; :: thesis: verum