let n be Nat; :: thesis: for K being commutative Ring
for A, B, C being Matrix of n,K
for i being Nat st i in Seg n holds
ex P being FinSequence of K st
( len P = n & Det (RLine (C,i,(Line ((A * B),i)))) = the addF of K "**" P & ( for j being Nat st j in Seg n holds
P . j = (A * (i,j)) * (Det (RLine (C,i,(Line (B,j))))) ) )
let K be commutative Ring; :: thesis: for A, B, C being Matrix of n,K
for i being Nat st i in Seg n holds
ex P being FinSequence of K st
( len P = n & Det (RLine (C,i,(Line ((A * B),i)))) = the addF of K "**" P & ( for j being Nat st j in Seg n holds
P . j = (A * (i,j)) * (Det (RLine (C,i,(Line (B,j))))) ) )
let A, B, C be Matrix of n,K; :: thesis: for i being Nat st i in Seg n holds
ex P being FinSequence of K st
( len P = n & Det (RLine (C,i,(Line ((A * B),i)))) = the addF of K "**" P & ( for j being Nat st j in Seg n holds
P . j = (A * (i,j)) * (Det (RLine (C,i,(Line (B,j))))) ) )
let i be Nat; :: thesis: ( i in Seg n implies ex P being FinSequence of K st
( len P = n & Det (RLine (C,i,(Line ((A * B),i)))) = the addF of K "**" P & ( for j being Nat st j in Seg n holds
P . j = (A * (i,j)) * (Det (RLine (C,i,(Line (B,j))))) ) ) )
assume A1: i in Seg n ; :: thesis: ex P being FinSequence of K st
( len P = n & Det (RLine (C,i,(Line ((A * B),i)))) = the addF of K "**" P & ( for j being Nat st j in Seg n holds
P . j = (A * (i,j)) * (Det (RLine (C,i,(Line (B,j))))) ) )
Seg n <> {} by A1;
then A2: n <> 0 ;
set a = addFinS K;
A3: len B = n by MATRIX_0:24;
deffunc H1( 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;
A4: len A = n by MATRIX_0:24;
consider D being FinSequence of the carrier of K such that
A5: len D = len A and
A6: for j being Nat st j in dom D holds
D . j = H1(j) from FINSEQ_2:sch 1();
 A7: n <> 0 by A1;
then len D >= 1 by A4, A5, NAT_1:14;
then consider Fd being sequence of the carrier of K such that
A8: Fd . 1 = D . 1 and
A9: for k being Nat st 0 <> k & k < n holds
Fd . (k + 1) = the addF of K . ((Fd . k),(D . (k + 1))) and
A10: the addF of K "**" D = Fd . n by A4, A5, FINSOP_1:def 1;
A11: dom D = Seg (len A) by A5, FINSEQ_1:def 3;
width A = n by MATRIX_0:24;
then consider P being FinSequence of the carrier of K * such that
A12: len P = n and
A13: Line ((A * B),i) = (addFinS K) "**" P and
A14: for j being Nat st j in Seg (len B) holds
P . j = (A * (i,j)) * (Line (B,j)) by A1, A7, A3, A4, Th55;
len P >= 1 by A12, A2, NAT_1:14;
then consider Fp being sequence of ( the carrier of K *) such that
A15: Fp . 1 = P . 1 and
A16: for k being Nat st 0 <> k & k < n holds
Fp . (k + 1) = (addFinS K) . ((Fp . k),(P . (k + 1))) and
A17: Line ((A * B),i) = Fp . n by A12, A13, FINSOP_1:def 1;
defpred S1[ 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)) ) );
A18: width B = n by MATRIX_0:24;
A19: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A20: S1[k] ; :: thesis: S1[k + 1]
set k1 = k + 1;
set A9 = A * (i,(k + 1));
set L = Line (B,(k + 1));
assume that
A21: 1 <= k + 1 and
A22: k + 1 <= n ; :: thesis: for pK being FinSequence of K st pK = Fp . (k + 1) holds
( len pK = n & Fd . (k + 1) = Det (RLine (C,i,pK)) )
A23: k + 1 in Seg n by A21, A22;
let Fpk1 be FinSequence of the carrier of K; :: thesis: ( Fpk1 = Fp . (k + 1) implies ( len Fpk1 = n & Fd . (k + 1) = Det (RLine (C,i,Fpk1)) ) )
assume A24: Fpk1 = Fp . (k + 1) ; :: thesis: ( len Fpk1 = n & Fd . (k + 1) = Det (RLine (C,i,Fpk1)) )
per cases ( k = 0 or k > 0 ) ;
suppose A25: k = 0 ; :: thesis: ( len Fpk1 = n & Fd . (k + 1) = Det (RLine (C,i,Fpk1)) )
A26: P . (k + 1) = (A * (i,(k + 1))) * (Line (B,(k + 1))) by A3, A14, A23;
A27: len (Line (B,(k + 1))) = n by A18, MATRIX_0:def 7;
D . (k + 1) = H1(1) by A4, A6, A11, A23, A25;
hence ( len Fpk1 = n & Fd . (k + 1) = Det (RLine (C,i,Fpk1)) ) by A1, A15, A8, A24, A25, A26, A27, Lm5, Th34; :: thesis: verum
end;
suppose A28: k > 0 ; :: thesis: ( len Fpk1 = n & Fd . (k + 1) = Det (RLine (C,i,Fpk1)) )
k + 1 in dom P by A12, A23, FINSEQ_1:def 3;
then A29: P . (k + 1) in rng P by FUNCT_1:def 3;
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 A29, FINSEQ_1:def 11;
A30: k + 0 < k + 1 by XREAL_1:8;
then A31: Fd . k = Det (RLine (C,i,Fpk)) by A20, A22, A28, NAT_1:14, XXREAL_0:2;
A32: len Fpk = n by A20, A22, A28, A30, NAT_1:14, XXREAL_0:2;
A33: k < n by A22, A30, XXREAL_0:2;
then A34: Fd . (k + 1) = the addF of K . ((Fd . k),(D . (k + 1))) by A9, A28;
A35: P . (k + 1) = (A * (i,(k + 1))) * (Line (B,(k + 1))) by A3, A14, A23;
Fpk1 = (addFinS K) . (Fpk,Pk1) by A16, A24, A28, A33;
then A36: Fpk1 = Fpk + ((A * (i,(k + 1))) * (Line (B,(k + 1)))) by A35, Def5;
A37: len (Line (B,(k + 1))) = n by A18, MATRIX_0:def 7;
then A38: 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, A37, 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, A32, A36, A38, Th36;
hence ( len Fpk1 = n & Fd . (k + 1) = Det (RLine (C,i,Fpk1)) ) by A4, A6, A11, A23, A31, A34, A32, A36, A38, Lm6; :: thesis: verum
end;
end;
end;
take D ; :: thesis: ( len D = n & 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))))) ) )
thus len D = n by A5, MATRIX_0:24; :: thesis: ( 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))))) ) )
A39: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch 2(A39, A19);
 then S1[ 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 A4, A12, A6, A11, A17, A10, A2, NAT_1:14; :: thesis: verum