let n be Nat; :: thesis:
let K be Field; :: thesis:
let A, B, C be Matrix of n,K; :: thesis:
let i be Nat; :: thesis:
assume A1: i in Seg n ; :: thesis:
Seg n <> {} by A1;
then B2: n <> 0 ;
set a = addFinS K;
A2: len B = n by MATRIX_1:25;
deffunc H₁( Nat) -> Element of the carrier of K = (A * i,$1) * (Det (RLine C,i,(Line B,$1)));
set aa = the addF of K;
set KK = the carrier of K;
A3: len A = n by MATRIX_1:25;
consider D being FinSequence of the carrier of K such that
A4: len D = len A and
A5: for j being Nat st j in dom D holds
D . j = H₁(j) from FINSEQ_2:sch 1();
A6: n <> 0 by A1;
then len D >= 1 by A3, A4, NAT_1:14;
then consider Fd being Function of NAT ,the carrier of K such that
A7: Fd . 1 = D . 1 and
A8: for k being Element of NAT st 0 <> k & k < n holds
Fd . (k + 1) = the addF of K . (Fd . k),(D . (k + 1)) and
A9: the addF of K "**" D = Fd . n by A3, A4, FINSOP_1:def 1;
A10: dom D = Seg (len A) by A4, FINSEQ_1:def 3;
width A = n by MATRIX_1:25;
then consider P being FinSequence of the carrier of K * such that
A11: len P = n and
A12: Line (A * B),i = (addFinS K) "**" P and
A13: for j being Nat st j in Seg (len B) holds
P . j = (A * i,j) * (Line B,j) by A1, A6, A2, A3, Th55;
len P >= 1 by A11, B2, NAT_1:14;
then consider Fp being Function of NAT ,(the carrier of K * ) such that
A14: Fp . 1 = P . 1 and
A15: for k being Element of NAT st 0 <> k & k < n holds
Fp . (k + 1) = (addFinS K) . (Fp . k),(P . (k + 1)) and
A16: Line (A * B),i = Fp . n by A11, A12, FINSOP_1:def 1;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= n implies for pK being FinSequence of K st pK = Fp . $1 holds
( len pK = n & Fd . $1 = Det (RLine C,i,pK) ) );
A17: width B = n by MATRIX_1:25;
A18: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A19: S₁[k] ; :: thesis:
set k1 = k + 1;
set A9 = A * i,(k + 1);
set L = Line B,(k + 1);
assume that
A20: 1 <= k + 1 and
A21: k + 1 <= n ; :: thesis:
A22: k + 1 in Seg n by A20, A21;
let Fpk1 be FinSequence of the carrier of K; :: thesis:
assume A23: Fpk1 = Fp . (k + 1) ; :: thesis:

per cases ;

suppose A24: k = 0 ; :: thesis:

A25: P . (k + 1) = (A * i,(k + 1)) * (Line B,(k + 1)) by A2, A13, A22;
A26: len (Line B,(k + 1)) = n by A17, MATRIX_1:def 8;
D . (k + 1) = H₁(1) by A3, A5, A10, A22, A24;
hence ( len Fpk1 = n & Fd . (k + 1) = Det (RLine C,i,Fpk1) ) by A1, A14, A7, A23, A24, A25, A26, Lm5, Th34; :: thesis:

end;

suppose A27: k > 0 ; :: thesis:

k + 1 in dom P by A11, A22, FINSEQ_1:def 3;
then A28: P . (k + 1) in rng P by FUNCT_1:def 5;
rng P c= the carrier of K * by FINSEQ_1:def 4;
then reconsider Pk1 = P . (k + 1), Fpk = Fp . k as Element of the carrier of K * by A28;
A29: k + 0 < k + 1 by XREAL_1:10;
then A30: Fd . k = Det (RLine C,i,Fpk) by A19, A21, A27, NAT_1:14, XXREAL_0:2;
A31: len Fpk = n by A19, A21, A27, A29, NAT_1:14, XXREAL_0:2;
A32: k < n by A21, A29, XXREAL_0:2;
then A33: Fd . (k + 1) = the addF of K . (Fd . k),(D . (k + 1)) by A8, A27;
A34: P . (k + 1) = (A * i,(k + 1)) * (Line B,(k + 1)) by A2, A13, A22;
Fpk1 = (addFinS K) . Fpk,Pk1 by A15, A23, A27, A32;
then A35: Fpk1 = Fpk + ((A * i,(k + 1)) * (Line B,(k + 1))) by A34, Def5;
A36: len (Line B,(k + 1)) = n by A17, MATRIX_1:def 8;
then A37: len ((A * i,(k + 1)) * (Line B,(k + 1))) = n by Lm5;
Det (RLine C,i,((A * i,(k + 1)) * (Line B,(k + 1)))) = (A * i,(k + 1)) * (Det (RLine C,i,(Line B,(k + 1)))) by A1, A36, Th34;
then Det (RLine C,i,Fpk1) = (Det (RLine C,i,Fpk)) + ((A * i,(k + 1)) * (Det (RLine C,i,(Line B,(k + 1))))) by A1, A31, A35, A37, Th36;
hence ( len Fpk1 = n & Fd . (k + 1) = Det (RLine C,i,Fpk1) ) by A3, A5, A10, A22, A30, A33, A31, A35, A37, Lm6; :: thesis:

end;

take D ; :: thesis:
thus len D = n by A4, MATRIX_1:25; :: thesis:
A38: S₁[ 0 ] ;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A38, A18);
then S₁[ len P] ;
hence ( Det (RLine C,i,(Line (A * B),i)) = the addF of K "**" D & ( for j being Nat st j in Seg n holds
D . j = (A * i,j) * (Det (RLine C,i,(Line B,j))) ) ) by A3, A11, A5, A10, A16, A9, B2, NAT_1:14; :: thesis: