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