defpred S₁[ Nat] means for M being Matrix of $1,F_Real st M is Matrix of $1,F_Rat holds
Det M in F_Rat ;
P0: S₁[ 0 ]

proof

let M be Matrix of 0 ,F_Real; :: thesis: ( M is Matrix of 0 ,F_Rat implies Det M in F_Rat )
assume M is Matrix of 0 ,F_Rat ; :: thesis: Det M in F_Rat
Det M = 1. F_Real by MATRIXR2:41
.= 1 ;
hence Det M in F_Rat ; :: thesis: verum

end;

P1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume P10: S₁[n] ; :: thesis: S₁[n + 1]
let M be Matrix of n + 1,F_Real; :: thesis: ( M is Matrix of n + 1,F_Rat implies Det M in F_Rat )
assume AS1: M is Matrix of n + 1,F_Rat ; :: thesis: Det M in F_Rat
reconsider j = 1 as Nat ;
X0: ( 1 <= 1 & 1 <= n + 1 ) by NAT_1:14;
then j in Seg (n + 1) ;
then X1: Det M = Sum (LaplaceExpC (M,j)) by LAPLACE:27;
set L = LaplaceExpC (M,j);
X2: ( len (LaplaceExpC (M,j)) = n + 1 & ( for i being Nat st i in dom (LaplaceExpC (M,j)) holds
(LaplaceExpC (M,j)) . i = (M * (i,j)) * (Cofactor (M,i,j)) ) ) by LAPLACE:def 8;
for i being Nat st i in dom (LaplaceExpC (M,j)) holds
(LaplaceExpC (M,j)) . i in F_Rat

proof

let i be Nat; :: thesis: ( i in dom (LaplaceExpC (M,j)) implies (LaplaceExpC (M,j)) . i in F_Rat )
assume X30: i in dom (LaplaceExpC (M,j)) ; :: thesis: (LaplaceExpC (M,j)) . i in F_Rat
then X31: (LaplaceExpC (M,j)) . i = (M * (i,j)) * (Cofactor (M,i,j)) by LAPLACE:def 8;
( i in Seg (n + 1) & j in Seg (n + 1) ) by X0, X2, X30, FINSEQ_1:def 3;
then [i,j] in [:(Seg (n + 1)),(Seg (n + 1)):] by ZFMISC_1:87;
then X41: [i,j] in Indices M by MATRIX_0:24;
then X32: M * (i,j) is Element of F_Rat by AS1, ZMATRLIN:41;
(n + 1) -' 1 = n by NAT_D:34;
then reconsider DD = Delete (M,i,j) as Matrix of n,F_Real ;
Det DD in F_Rat

proof

per cases ( 0 < n or not 0 < n ) ;

suppose 0 < n ; :: thesis: Det DD in F_Rat

then DD is Matrix of n,F_Rat by LmSign1EX, AS1, X41;
hence Det DD in F_Rat by P10; :: thesis: verum

end;

suppose not 0 < n ; :: thesis: Det DD in F_Rat

then n = 0 ;
then Det DD = 1. F_Real by MATRIXR2:41
.= 1 ;
hence Det DD in F_Rat ; :: thesis: verum

end;

end;

end;

then A1: Minor (M,i,j) in F_Rat by NAT_D:34;
(power F_Real) . ((- (1_ F_Real)),(i + j)) in F_Rat by LmSign1D;
hence (LaplaceExpC (M,j)) . i in F_Rat by A1, X32, X31, RAT_1:def 2; :: thesis: verum

end;

hence Det M in F_Rat by X1, LmSign1C; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(P0, P1);
hence for n being Nat
for M being Matrix of n,F_Real st M is Matrix of n,F_Rat holds
Det M in F_Rat ; :: thesis: verum