defpred S1[ FinSequence of NAT , Nat, Nat, Matrix of F2(),F3(),F1()] means ( \$4 * (\$2,(\$1 /. \$2)) <> 0. F1() & ( \$3 in dom \$1 & \$2 < \$3 implies \$1 /. \$2 < \$1 /. \$3 ) & ( \$3 in (dom \$1) \ {\$2} implies \$4 * (\$3,(\$1 /. \$2)) = 0. F1() ) & ( \$3 in Seg (width \$4) & \$3 < \$1 /. \$2 implies \$4 * (\$2,\$3) = 0. F1() ) );
set r = the_rank_of F5();
ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ( for i being Nat st i in dom A9 & i > the_rank_of F5() holds
Line (A9,i) = F3() |-> (0. F1()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A9 & f is one-to-one & rng f c= Seg (width A9) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )
proof
per cases ( F2() = 0 or F2() > 0 ) ;
suppose A3: F2() = 0 ; :: thesis: ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ( for i being Nat st i in dom A9 & i > the_rank_of F5() holds
Line (A9,i) = F3() |-> (0. F1()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A9 & f is one-to-one & rng f c= Seg (width A9) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )

take A9 = F5(); :: thesis: ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ( for i being Nat st i in dom A9 & i > the_rank_of F5() holds
Line (A9,i) = F3() |-> (0. F1()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A9 & f is one-to-one & rng f c= Seg (width A9) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )

take B9 = F6(); :: thesis: ( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ( for i being Nat st i in dom A9 & i > the_rank_of F5() holds
Line (A9,i) = F3() |-> (0. F1()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A9 & f is one-to-one & rng f c= Seg (width A9) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )

( dom A9 = Seg (len A9) & len A9 = 0 ) by ;
hence ( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ( for i being Nat st i in dom A9 & i > the_rank_of F5() holds
Line (A9,i) = F3() |-> (0. F1()) ) ) by A1; :: thesis: ex f being FinSequence of NAT st
( len f = the_rank_of A9 & f is one-to-one & rng f c= Seg (width A9) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) )

take <*> NAT ; :: thesis: ( len () = the_rank_of A9 & <*> NAT is one-to-one & rng () c= Seg (width A9) & ( for i, j being Nat st i in dom () holds
S1[ <*> NAT,i,j,A9] ) )

len A9 = 0 by ;
hence ( len () = the_rank_of A9 & <*> NAT is one-to-one & rng () c= Seg (width A9) & ( for i, j being Nat st i in dom () holds
S1[ <*> NAT,i,j,A9] ) ) by MATRIX13:74; :: thesis: verum
end;
suppose A4: F2() > 0 ; :: thesis: ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ( for i being Nat st i in dom A9 & i > the_rank_of F5() holds
Line (A9,i) = F3() |-> (0. F1()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A9 & f is one-to-one & rng f c= Seg (width A9) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )

defpred S2[ Nat] means ( \$1 <= F3() implies ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= \$1 holds
A9 * (i,j) = 0. F1() ) & f is one-to-one & len f <= \$1 & len f <= F2() & rng f c= Seg \$1 & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) ) );
A5: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A6: S2[n] ; :: thesis: S2[n + 1]
set n1 = n + 1;
assume A7: n + 1 <= F3() ; :: thesis: ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n + 1 holds
A9 * (i,j) = 0. F1() ) & f is one-to-one & len f <= n + 1 & len f <= F2() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )

then consider A9 being Matrix of F2(),F3(),F1(), B9 being Matrix of F2(),F4(),F1() such that
A8: ( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 ) and
A9: ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & f is one-to-one & len f <= n & len f <= F2() & rng f c= Seg n & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) by ;
consider f being FinSequence of NAT such that
A10: for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() and
A11: f is one-to-one and
A12: len f <= n and
A13: len f <= F2() and
A14: rng f c= Seg n and
A15: for i, j being Nat st i in dom f holds
S1[f,i,j,A9] by A9;
per cases ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j = n + 1 holds
A9 * (i,j) = 0. F1() or ex i, j being Nat st
( [i,j] in Indices A9 & i > len f & j = n + 1 & A9 * (i,j) <> 0. F1() ) )
;
suppose A16: for i, j being Nat st [i,j] in Indices A9 & i > len f & j = n + 1 holds
A9 * (i,j) = 0. F1() ; :: thesis: ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n + 1 holds
A9 * (i,j) = 0. F1() ) & f is one-to-one & len f <= n + 1 & len f <= F2() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )

A17: now :: thesis: for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n + 1 holds
A9 * (i,j) = 0. F1()
let i, j be Nat; :: thesis: ( [i,j] in Indices A9 & i > len f & j <= n + 1 implies A9 * (i,j) = 0. F1() )
assume that
A18: ( [i,j] in Indices A9 & i > len f ) and
A19: j <= n + 1 ; :: thesis: A9 * (i,j) = 0. F1()
( j <= n or j = n + 1 ) by ;
hence A9 * (i,j) = 0. F1() by ; :: thesis: verum
end;
n <= n + 1 by NAT_1:13;
then Seg n c= Seg (n + 1) by FINSEQ_1:5;
then A20: rng f c= Seg (n + 1) by A14;
len f <= n + 1 by ;
hence ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n + 1 holds
A9 * (i,j) = 0. F1() ) & f is one-to-one & len f <= n + 1 & len f <= F2() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) ) by A8, A11, A13, A15, A17, A20; :: thesis: verum
end;
suppose ex i, j being Nat st
( [i,j] in Indices A9 & i > len f & j = n + 1 & A9 * (i,j) <> 0. F1() ) ; :: thesis: ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n + 1 holds
A9 * (i,j) = 0. F1() ) & f is one-to-one & len f <= n + 1 & len f <= F2() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )

then consider i0, j0 being Nat such that
A21: [i0,j0] in Indices A9 and
A22: i0 > len f and
A23: j0 = n + 1 and
A24: A9 * (i0,j0) <> 0. F1() ;
A25: Indices A9 = [:(Seg F2()),(Seg F3()):] by ;
then A26: n + 1 in Seg F3() by ;
A27: i0 in Seg F2() by ;
then A28: i0 <= F2() by FINSEQ_1:1;
A29: (len f) + 1 <= i0 by ;
then ( 0 + 1 <= (len f) + 1 & (len f) + 1 <= F2() ) by ;
then A30: (len f) + 1 in Seg F2() ;
defpred S3[ Nat] means ( \$1 <= F2() implies ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= \$1 holds
A9 * (j,(n + 1)) = 0. F1() ) ) );
A31: dom f = Seg (len f) by FINSEQ_1:def 3;
n <= F3() by ;
then A32: Seg n c= Seg F3() by FINSEQ_1:5;
A33: Seg (len f) c= Seg F2() by ;
A34: for k being Nat st S3[k] holds
S3[k + 1]
proof
let k be Nat; :: thesis: ( S3[k] implies S3[k + 1] )
assume A35: S3[k] ; :: thesis: S3[k + 1]
set k1 = k + 1;
assume k + 1 <= F2() ; :: thesis: ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= k + 1 holds
A9 * (j,(n + 1)) = 0. F1() ) )

then consider AA being Matrix of F2(),F3(),F1(), BB being Matrix of F2(),F4(),F1() such that
A36: P1[AA,BB] and
A37: the_rank_of F5() = the_rank_of AA and
A38: AA * (((len f) + 1),(n + 1)) <> 0. F1() and
A39: for i, j being Nat st [i,j] in Indices AA & i > len f & j <= n holds
AA * (i,j) = 0. F1() and
A40: for i, j being Nat st i in dom f holds
S1[f,i,j,AA] and
A41: for j being Nat st j in (dom AA) \ {((len f) + 1)} & j <= k holds
AA * (j,(n + 1)) = 0. F1() by ;
now :: thesis: ex RA being Matrix of F2(),F3(),F1() ex RB being Matrix of F2(),F4(),F1() ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= k + 1 holds
A9 * (j,(n + 1)) = 0. F1() ) )
per cases ( k + 1 = (len f) + 1 or k + 1 <> (len f) + 1 ) ;
suppose A42: k + 1 = (len f) + 1 ; :: thesis: ex RA being Matrix of F2(),F3(),F1() ex RB being Matrix of F2(),F4(),F1() ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= k + 1 holds
A9 * (j,(n + 1)) = 0. F1() ) )

take RA = AA; :: thesis: ex RB being Matrix of F2(),F4(),F1() ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= k + 1 holds
A9 * (j,(n + 1)) = 0. F1() ) )

take RB = BB; :: thesis: ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= k + 1 holds
A9 * (j,(n + 1)) = 0. F1() ) )

now :: thesis: for j being Nat st j in (dom RA) \ {((len f) + 1)} & j <= k + 1 holds
RA * (j,(n + 1)) = 0. F1()
let j be Nat; :: thesis: ( j in (dom RA) \ {((len f) + 1)} & j <= k + 1 implies RA * (j,(n + 1)) = 0. F1() )
assume that
A43: j in (dom RA) \ {((len f) + 1)} and
A44: j <= k + 1 ; :: thesis: RA * (j,(n + 1)) = 0. F1()
j <> (len f) + 1 by ;
then j < k + 1 by ;
then j <= k by NAT_1:13;
hence RA * (j,(n + 1)) = 0. F1() by ; :: thesis: verum
end;
hence ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= k + 1 holds
A9 * (j,(n + 1)) = 0. F1() ) ) by A36, A37, A38, A39, A40; :: thesis: verum
end;
suppose A45: k + 1 <> (len f) + 1 ; :: thesis: ex RA being FinSequence of the carrier of F1() * ex RB being Matrix of F2(),F4(),F1() ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= k + 1 holds
A9 * (j,(n + 1)) = 0. F1() ) )

set LA = Line (AA,(k + 1));
set LAf = Line (AA,((len f) + 1));
set a = AA * (((len f) + 1),(n + 1));
set RA = RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))));
A46: width AA = F3() by ;
then A47: len ((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))) = F3() by CARD_1:def 7;
A48: Indices A9 = Indices AA by MATRIX_0:26;
then [((len f) + 1),(n + 1)] in Indices AA by ;
then A49: (RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))))) * (((len f) + 1),(n + 1)) <> 0. F1() by ;
A50: Indices A9 = Indices (RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))))) by MATRIX_0:26;
A51: now :: thesis: for i, j being Nat st [i,j] in Indices (RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))))) & i > len f & j <= n holds
(RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))))) * (i,j) = 0. F1()
let i, j be Nat; :: thesis: ( [i,j] in Indices (RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))))) & i > len f & j <= n implies (RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))))) * (i,j) = 0. F1() )
assume that
A52: [i,j] in Indices (RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))))) and
A53: i > len f and
A54: j <= n ; :: thesis: (RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))))) * (i,j) = 0. F1()
now :: thesis: (RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))))) * (i,j) = 0. F1()
per cases ( i = k + 1 or i <> k + 1 ) ;
suppose A55: i = k + 1 ; :: thesis: (RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))))) * (i,j) = 0. F1()
A56: j in Seg F3() by ;
then ( (len f) + 1 > len f & [((len f) + 1),j] in Indices A9 ) by ;
then AA * (((len f) + 1),j) = 0. F1() by ;
then (Line (AA,((len f) + 1))) . j = 0. F1() by ;
then A57: ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1)))) . j = (- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (0. F1()) by
.= 0. F1() ;
(Line (AA,(k + 1))) . j = AA * ((k + 1),j) by
.= 0. F1() by A39, A48, A50, A52, A53, A54, A55 ;
then (0. F1()) + (0. F1()) = ((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))) . j by
.= (RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))))) * (i,j) by ;
hence (RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))))) * (i,j) = 0. F1() by RLVECT_1:def 4; :: thesis: verum
end;
suppose i <> k + 1 ; :: thesis: (RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))))) * (i,j) = 0. F1()
hence (RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))))) * (i,j) = AA * (i,j) by
.= 0. F1() by A39, A48, A50, A52, A53, A54 ;
:: thesis: verum
end;
end;
end;
hence (RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))))) * (i,j) = 0. F1() ; :: thesis: verum
end;
set RB = F7(BB,(k + 1),((len f) + 1),(- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))));
take RA = RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1)))))); :: thesis: ex RB being Matrix of F2(),F4(),F1() ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= k + 1 holds
A9 * (j,(n + 1)) = 0. F1() ) )

take RB = F7(BB,(k + 1),((len f) + 1),(- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) ")))); :: thesis: ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= k + 1 holds
A9 * (j,(n + 1)) = 0. F1() ) )

A58: width RA = F3() by ;
A59: len AA = F2() by MATRIX_0:def 2;
A60: now :: thesis: for j being Nat st j in (dom RA) \ {((len f) + 1)} & j <= k + 1 holds
RA * (j,(n + 1)) = 0. F1()
A61: dom AA = Seg (len AA) by FINSEQ_1:def 3;
let j be Nat; :: thesis: ( j in (dom RA) \ {((len f) + 1)} & j <= k + 1 implies RA * (j,(n + 1)) = 0. F1() )
assume that
A62: j in (dom RA) \ {((len f) + 1)} and
A63: j <= k + 1 ; :: thesis: RA * (j,(n + 1)) = 0. F1()
j in dom RA by ;
then A64: [j,(n + 1)] in Indices AA by ;
A65: ( dom RA = Seg (len RA) & len RA = F2() ) by ;
now :: thesis: RA * (j,(n + 1)) = 0. F1()
per cases ( j <= k or j = k + 1 ) by ;
suppose A66: j <= k ; :: thesis: RA * (j,(n + 1)) = 0. F1()
then j < k + 1 by NAT_1:13;
hence RA * (j,(n + 1)) = AA * (j,(n + 1)) by
.= 0. F1() by A41, A59, A62, A65, A61, A66 ;
:: thesis: verum
end;
suppose A67: j = k + 1 ; :: thesis: RA * (j,(n + 1)) = 0. F1()
(Line (AA,((len f) + 1))) . (n + 1) = AA * (((len f) + 1),(n + 1)) by ;
then A68: ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1)))) . (n + 1) = (- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (AA * (((len f) + 1),(n + 1))) by
.= ((- (AA * ((k + 1),(n + 1)))) * ((AA * (((len f) + 1),(n + 1))) ")) * (AA * (((len f) + 1),(n + 1))) by VECTSP_1:9
.= (- (AA * ((k + 1),(n + 1)))) * (((AA * (((len f) + 1),(n + 1))) ") * (AA * (((len f) + 1),(n + 1)))) by GROUP_1:def 3
.= (- (AA * ((k + 1),(n + 1)))) * (1_ F1()) by
.= - (AA * ((k + 1),(n + 1))) ;
(Line (AA,(k + 1))) . (n + 1) = AA * ((k + 1),(n + 1)) by ;
then ((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))) . (n + 1) = (AA * ((k + 1),(n + 1))) + (- (AA * ((k + 1),(n + 1)))) by
.= 0. F1() by VECTSP_1:19 ;
hence RA * (j,(n + 1)) = 0. F1() by ; :: thesis: verum
end;
end;
end;
hence RA * (j,(n + 1)) = 0. F1() ; :: thesis: verum
end;
A69: dom AA = Seg (len AA) by FINSEQ_1:def 3;
A70: now :: thesis: for i, j being Nat st i in dom f holds
( RA * (i,(f /. i)) <> 0. F1() & ( j in dom f & i < j implies f /. i < f /. j ) & ( j in (dom f) \ {i} implies RA * (j,(f /. i)) = 0. F1() ) & ( j in Seg (width RA) & j < f /. i implies RA * (i,j) = 0. F1() ) )
let i, j be Nat; :: thesis: ( i in dom f implies ( RA * (i,(f /. i)) <> 0. F1() & ( j in dom f & i < j implies f /. i < f /. j ) & ( j in (dom f) \ {i} implies RA * (j,(f /. i)) = 0. F1() ) & ( j in Seg (width RA) & j < f /. i implies RA * (i,j) = 0. F1() ) ) )
assume A71: i in dom f ; :: thesis: ( RA * (i,(f /. i)) <> 0. F1() & ( j in dom f & i < j implies f /. i < f /. j ) & ( j in (dom f) \ {i} implies RA * (j,(f /. i)) = 0. F1() ) & ( j in Seg (width RA) & j < f /. i implies RA * (i,j) = 0. F1() ) )
set fi = f /. i;
A72: ( f /. i = f . i & f . i in rng f ) by ;
then A73: f /. i in Seg n by A14;
A74: ( (len f) + 1 > len f & f /. i <= n ) by ;
( [((len f) + 1),(f /. i)] in Indices AA & (Line (AA,((len f) + 1))) . (f /. i) = AA * (((len f) + 1),(f /. i)) ) by ;
then (Line (AA,((len f) + 1))) . (f /. i) = 0. F1() by ;
then A75: ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1)))) . (f /. i) = (- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (0. F1()) by
.= 0. F1() ;
(Line (AA,(k + 1))) . (f /. i) = AA * ((k + 1),(f /. i)) by ;
then A76: ((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))) . (f /. i) = (AA * ((k + 1),(f /. i))) + (0. F1()) by
.= AA * ((k + 1),(f /. i)) by RLVECT_1:def 4 ;
A77: [i,(f /. i)] in Indices AA by ;
now :: thesis: RA * (i,(f /. i)) <> 0. F1()
per cases ( i <> k + 1 or i = k + 1 ) ;
suppose i <> k + 1 ; :: thesis: RA * (i,(f /. i)) <> 0. F1()
then RA * (i,(f /. i)) = AA * (i,(f /. i)) by ;
hence RA * (i,(f /. i)) <> 0. F1() by ; :: thesis: verum
end;
suppose i = k + 1 ; :: thesis: RA * (i,(f /. i)) <> 0. F1()
then RA * (i,(f /. i)) = AA * (i,(f /. i)) by ;
hence RA * (i,(f /. i)) <> 0. F1() by ; :: thesis: verum
end;
end;
end;
hence ( RA * (i,(f /. i)) <> 0. F1() & ( j in dom f & i < j implies f /. i < f /. j ) ) by ; :: thesis: ( ( j in (dom f) \ {i} implies RA * (j,(f /. i)) = 0. F1() ) & ( j in Seg (width RA) & j < f /. i implies RA * (i,j) = 0. F1() ) )
thus ( j in (dom f) \ {i} implies RA * (j,(f /. i)) = 0. F1() ) :: thesis: ( j in Seg (width RA) & j < f /. i implies RA * (i,j) = 0. F1() )
proof
assume A78: j in (dom f) \ {i} ; :: thesis: RA * (j,(f /. i)) = 0. F1()
then j in Seg (len f) by ;
then A79: [j,(f /. i)] in Indices AA by ;
per cases ( j <> k + 1 or j = k + 1 ) ;
suppose j <> k + 1 ; :: thesis: RA * (j,(f /. i)) = 0. F1()
hence RA * (j,(f /. i)) = AA * (j,(f /. i)) by
.= 0. F1() by ;
:: thesis: verum
end;
suppose A80: j = k + 1 ; :: thesis: RA * (j,(f /. i)) = 0. F1()
hence RA * (j,(f /. i)) = ((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))) . (f /. i) by
.= 0. F1() by A40, A71, A76, A78, A80 ;
:: thesis: verum
end;
end;
end;
thus ( j in Seg (width RA) & j < f /. i implies RA * (i,j) = 0. F1() ) :: thesis: verum
proof
assume that
A81: j in Seg (width RA) and
A82: j < f /. i ; :: thesis: RA * (i,j) = 0. F1()
A83: [((len f) + 1),j] in Indices AA by ;
A84: [i,j] in Indices AA by ;
per cases ( i <> k + 1 or i = k + 1 ) ;
suppose i <> k + 1 ; :: thesis: RA * (i,j) = 0. F1()
hence RA * (i,j) = AA * (i,j) by
.= 0. F1() by A40, A46, A58, A71, A81, A82 ;
:: thesis: verum
end;
suppose A85: i = k + 1 ; :: thesis: RA * (i,j) = 0. F1()
f /. i <= n by ;
then A86: j <= n by ;
(len f) + 1 > len f by NAT_1:13;
then 0. F1() = AA * (((len f) + 1),j) by
.= (Line (AA,((len f) + 1))) . j by ;
then A87: ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1)))) . j = (- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (0. F1()) by
.= 0. F1() ;
(Line (AA,(k + 1))) . j = AA * (i,j) by
.= 0. F1() by A40, A46, A58, A71, A81, A82 ;
then ((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))) . j = (0. F1()) + (0. F1()) by
.= 0. F1() by RLVECT_1:def 4 ;
hence RA * (i,j) = 0. F1() by ; :: thesis: verum
end;
end;
end;
end;
A88: (len f) + 1 in Seg (len AA) by ;
then A89: the_rank_of F5() = the_rank_of RA by ;
P1[RA,RB] by A2, A36, A45, A88, A69;
hence ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= k + 1 holds
A9 * (j,(n + 1)) = 0. F1() ) ) by A89, A49, A51, A70, A60; :: thesis: verum
end;
end;
end;
hence ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= k + 1 holds
A9 * (j,(n + 1)) = 0. F1() ) ) ; :: thesis: verum
end;
A90: j0 in Seg F3() by ;
ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) )
proof
per cases ( A9 * (((len f) + 1),(n + 1)) <> 0. F1() or A9 * (((len f) + 1),(n + 1)) = 0. F1() ) ;
suppose A9 * (((len f) + 1),(n + 1)) <> 0. F1() ; :: thesis: ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) )

hence ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) by A8, A10, A15; :: thesis: verum
end;
suppose A91: A9 * (((len f) + 1),(n + 1)) = 0. F1() ; :: thesis: ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) )

set RB = F7(B9,((len f) + 1),i0,(1_ F1()));
set LA = Line (A9,i0);
set LAf = Line (A9,((len f) + 1));
set RA = RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))));
take RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0))))) ; :: thesis: ex B9 being Matrix of F2(),F4(),F1() st
( P1[ RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0))))),B9] & the_rank_of F5() = the_rank_of (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) & (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) & i > len f & j <= n holds
(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j, RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))] ) )

take F7(B9,((len f) + 1),i0,(1_ F1())) ; :: thesis: ( P1[ RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0))))),F7(B9,((len f) + 1),i0,(1_ F1()))] & the_rank_of F5() = the_rank_of (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) & (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) & i > len f & j <= n holds
(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j, RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))] ) )

( i0 in dom A9 & dom A9 = Seg (len A9) ) by ;
hence ( P1[ RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0))))),F7(B9,((len f) + 1),i0,(1_ F1()))] & the_rank_of F5() = the_rank_of (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) ) by ; :: thesis: ( (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) & i > len f & j <= n holds
(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j, RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))] ) )

A92: ( (1_ F1()) * (Line (A9,i0)) = Line (A9,i0) & len ((Line (A9,((len f) + 1))) + (Line (A9,i0))) = width A9 ) by ;
[((len f) + 1),j0] in Indices A9 by ;
then A93: (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (((len f) + 1),(n + 1)) = ((Line (A9,((len f) + 1))) + (Line (A9,i0))) . (n + 1) by ;
A94: width A9 = F3() by ;
then A95: (Line (A9,i0)) . (n + 1) = A9 * (i0,(n + 1)) by ;
(Line (A9,((len f) + 1))) . (n + 1) = 0. F1() by ;
then (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (((len f) + 1),(n + 1)) = (0. F1()) + (A9 * (i0,(n + 1))) by
.= A9 * (i0,(n + 1)) by RLVECT_1:def 4 ;
hence (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (((len f) + 1),(n + 1)) <> 0. F1() by ; :: thesis: ( ( for i, j being Nat st [i,j] in Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) & i > len f & j <= n holds
(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j, RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))] ) )

A96: Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) = Indices A9 by MATRIX_0:26;
now :: thesis: for i, j being Nat st [i,j] in Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) & i > len f & j <= n holds
(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1()
let i, j be Nat; :: thesis: ( [i,j] in Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) & i > len f & j <= n implies (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1() )
assume that
A97: [i,j] in Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) and
A98: i > len f and
A99: j <= n ; :: thesis: (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1()
A100: j in Seg F3() by ;
A101: i >= (len f) + 1 by ;
now :: thesis: (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1()
per cases ( i > (len f) + 1 or i = (len f) + 1 ) by ;
suppose i > (len f) + 1 ; :: thesis: (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1()
hence (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = A9 * (i,j) by
.= 0. F1() by A10, A96, A97, A98, A99 ;
:: thesis: verum
end;
suppose A102: i = (len f) + 1 ; :: thesis: (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1()
A103: [i0,j] in Indices A9 by ;
A104: ( (Line (A9,((len f) + 1))) . j = A9 * (((len f) + 1),j) & (Line (A9,i0)) . j = A9 * (i0,j) ) by ;
(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = ((Line (A9,((len f) + 1))) + (Line (A9,i0))) . j by ;
hence (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = (A9 * (((len f) + 1),j)) + (A9 * (i0,j)) by
.= (0. F1()) + (A9 * (i0,j)) by A10, A96, A97, A98, A99, A102
.= (0. F1()) + (0. F1()) by
.= 0. F1() by RLVECT_1:def 4 ;
:: thesis: verum
end;
end;
end;
hence (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1() ; :: thesis: verum
end;
hence for i, j being Nat st [i,j] in Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) & i > len f & j <= n holds
(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1() ; :: thesis: for i, j being Nat st i in dom f holds
S1[f,i,j, RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))]

let i, j be Nat; :: thesis: ( i in dom f implies S1[f,i,j, RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))] )
assume A105: i in dom f ; :: thesis: S1[f,i,j, RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))]
i <= len f by ;
then A106: i < (len f) + 1 by NAT_1:13;
( f /. i = f . i & f . i in rng f ) by ;
then A107: f /. i in Seg n by A14;
then [i,(f /. i)] in Indices A9 by ;
then (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,(f /. i)) = A9 * (i,(f /. i)) by ;
hence ( (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,(f /. i)) <> 0. F1() & ( j in dom f & i < j implies f /. i < f /. j ) ) by ; :: thesis: ( ( j in (dom f) \ {i} implies (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (j,(f /. i)) = 0. F1() ) & ( j in Seg (width (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0))))))) & j < f /. i implies (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1() ) )
thus ( j in (dom f) \ {i} implies (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (j,(f /. i)) = 0. F1() ) :: thesis: ( j in Seg (width (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0))))))) & j < f /. i implies (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1() )
proof
assume A108: j in (dom f) \ {i} ; :: thesis: (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (j,(f /. i)) = 0. F1()
then A109: j in dom f by XBOOLE_0:def 5;
then j <= len f by ;
then A110: j < (len f) + 1 by NAT_1:13;
[j,(f /. i)] in Indices A9 by ;
hence (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (j,(f /. i)) = A9 * (j,(f /. i)) by
.= 0. F1() by ;
:: thesis: verum
end;
assume that
A111: j in Seg (width (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0))))))) and
A112: j < f /. i ; :: thesis: (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1()
A113: width (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) = width A9 by ;
then [i,j] in Indices A9 by ;
hence (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = A9 * (i,j) by
.= 0. F1() by ;
:: thesis: verum
end;
end;
end;
then consider A0 being Matrix of F2(),F3(),F1(), B0 being Matrix of F2(),F4(),F1() such that
A114: ( P1[A0,B0] & the_rank_of F5() = the_rank_of A0 & A0 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A0 & i > len f & j <= n holds
A0 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A0] ) ) ;
A115: S3[ 0 ]
proof
assume 0 <= F2() ; :: thesis: ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= 0 holds
A9 * (j,(n + 1)) = 0. F1() ) )

take A0 ; :: thesis: ex B9 being Matrix of F2(),F4(),F1() st
( P1[A0,B9] & the_rank_of F5() = the_rank_of A0 & A0 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A0 & i > len f & j <= n holds
A0 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A0] ) & ( for j being Nat st j in (dom A0) \ {((len f) + 1)} & j <= 0 holds
A0 * (j,(n + 1)) = 0. F1() ) )

take B0 ; :: thesis: ( P1[A0,B0] & the_rank_of F5() = the_rank_of A0 & A0 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A0 & i > len f & j <= n holds
A0 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A0] ) & ( for j being Nat st j in (dom A0) \ {((len f) + 1)} & j <= 0 holds
A0 * (j,(n + 1)) = 0. F1() ) )

now :: thesis: for j being Nat st j in (dom A0) \ {((len f) + 1)} & j <= 0 holds
A0 * (j,(n + 1)) = 0. F1()
A116: dom A0 = Seg (len A0) by FINSEQ_1:def 3;
let j be Nat; :: thesis: ( j in (dom A0) \ {((len f) + 1)} & j <= 0 implies A0 * (j,(n + 1)) = 0. F1() )
assume ( j in (dom A0) \ {((len f) + 1)} & j <= 0 ) ; :: thesis: A0 * (j,(n + 1)) = 0. F1()
hence A0 * (j,(n + 1)) = 0. F1() by A116; :: thesis: verum
end;
hence ( P1[A0,B0] & the_rank_of F5() = the_rank_of A0 & A0 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A0 & i > len f & j <= n holds
A0 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A0] ) & ( for j being Nat st j in (dom A0) \ {((len f) + 1)} & j <= 0 holds
A0 * (j,(n + 1)) = 0. F1() ) ) by A114; :: thesis: verum
end;
for k being Nat holds S3[k] from then consider Aa being Matrix of F2(),F3(),F1(), Bb being Matrix of F2(),F4(),F1() such that
A117: ( P1[Aa,Bb] & the_rank_of F5() = the_rank_of Aa ) and
A118: Aa * (((len f) + 1),(n + 1)) <> 0. F1() and
A119: for i, j being Nat st [i,j] in Indices Aa & i > len f & j <= n holds
Aa * (i,j) = 0. F1() and
A120: for i, j being Nat st i in dom f holds
S1[f,i,j,Aa] and
A121: for j being Nat st j in (dom Aa) \ {((len f) + 1)} & j <= F2() holds
Aa * (j,(n + 1)) = 0. F1() ;
take Aa ; :: thesis: ex B9 being Matrix of F2(),F4(),F1() st
( P1[Aa,B9] & the_rank_of F5() = the_rank_of Aa & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices Aa & i > len f & j <= n + 1 holds
Aa * (i,j) = 0. F1() ) & f is one-to-one & len f <= n + 1 & len f <= F2() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,Aa] ) ) )

take Bb ; :: thesis: ( P1[Aa,Bb] & the_rank_of F5() = the_rank_of Aa & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices Aa & i > len f & j <= n + 1 holds
Aa * (i,j) = 0. F1() ) & f is one-to-one & len f <= n + 1 & len f <= F2() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,Aa] ) ) )

thus ( P1[Aa,Bb] & the_rank_of F5() = the_rank_of Aa ) by A117; :: thesis: ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices Aa & i > len f & j <= n + 1 holds
Aa * (i,j) = 0. F1() ) & f is one-to-one & len f <= n + 1 & len f <= F2() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,Aa] ) )

take f9 = f ^ <*(n + 1)*>; :: thesis: ( ( for i, j being Nat st [i,j] in Indices Aa & i > len f9 & j <= n + 1 holds
Aa * (i,j) = 0. F1() ) & f9 is one-to-one & len f9 <= n + 1 & len f9 <= F2() & rng f9 c= Seg (n + 1) & ( for i, j being Nat st i in dom f9 holds
S1[f9,i,j,Aa] ) )

A122: len f9 = (len f) + 1 by FINSEQ_2:16;
A123: ( len Aa = F2() & dom Aa = Seg (len Aa) ) by ;
A124: now :: thesis: for i, j being Nat st [i,j] in Indices Aa & i > len f9 & j <= n + 1 holds
Aa * (i,j) = 0. F1()
let i, j be Nat; :: thesis: ( [i,j] in Indices Aa & i > len f9 & j <= n + 1 implies Aa * (b1,b2) = 0. F1() )
assume that
A125: [i,j] in Indices Aa and
A126: i > len f9 and
A127: j <= n + 1 ; :: thesis: Aa * (b1,b2) = 0. F1()
per cases ( j <= n or j = n + 1 ) by ;
suppose A128: j <= n ; :: thesis: Aa * (b1,b2) = 0. F1()
i > len f by ;
hence Aa * (i,j) = 0. F1() by ; :: thesis: verum
end;
suppose A129: j = n + 1 ; :: thesis: Aa * (b1,b2) = 0. F1()
i in dom Aa by ;
then ( i in (dom Aa) \ {((len f) + 1)} & i <= F2() ) by ;
hence Aa * (i,j) = 0. F1() by ; :: thesis: verum
end;
end;
end;
A130: width Aa = F3() by ;
A131: len f9 <= F2() by ;
A132: now :: thesis: for i, j being Nat st i in dom f9 holds
( Aa * (i,(f9 /. i)) <> 0. F1() & ( j in dom f9 & i < j implies f9 /. i < f9 /. j ) & ( j in (dom f9) \ {i} implies Aa * (j,(f9 /. i)) = 0. F1() ) & ( j in Seg (width Aa) & j < f9 /. i implies Aa * (i,j) = 0. F1() ) )
let i, j be Nat; :: thesis: ( i in dom f9 implies ( Aa * (i,(f9 /. i)) <> 0. F1() & ( j in dom f9 & i < j implies f9 /. i < f9 /. j ) & ( j in (dom f9) \ {i} implies Aa * (j,(f9 /. i)) = 0. F1() ) & ( j in Seg (width Aa) & j < f9 /. i implies Aa * (i,j) = 0. F1() ) ) )
assume A133: i in dom f9 ; :: thesis: ( Aa * (i,(f9 /. i)) <> 0. F1() & ( j in dom f9 & i < j implies f9 /. i < f9 /. j ) & ( j in (dom f9) \ {i} implies Aa * (j,(f9 /. i)) = 0. F1() ) & ( j in Seg (width Aa) & j < f9 /. i implies Aa * (i,j) = 0. F1() ) )
A134: dom f9 = Seg ((len f) + 1) by
.= (dom f) \/ {((len f) + 1)} by ;
A135: now :: thesis: for k being Nat st k in dom f holds
f /. k = f9 /. k
let k be Nat; :: thesis: ( k in dom f implies f /. k = f9 /. k )
assume A136: k in dom f ; :: thesis: f /. k = f9 /. k
A137: k in dom f9 by ;
thus f /. k = f . k by
.= f9 . k by
.= f9 /. k by ; :: thesis: verum
end;
now :: thesis: Aa * (i,(f9 /. i)) <> 0. F1()
per cases ( i in dom f or i in {((len f) + 1)} ) by ;
suppose A138: i in dom f ; :: thesis: Aa * (i,(f9 /. i)) <> 0. F1()
then f /. i = f9 /. i by A135;
hence Aa * (i,(f9 /. i)) <> 0. F1() by ; :: thesis: verum
end;
suppose A139: i in {((len f) + 1)} ; :: thesis: Aa * (i,(f9 /. i)) <> 0. F1()
A140: f9 /. i = f9 . i by ;
i = (len f) + 1 by ;
hence Aa * (i,(f9 /. i)) <> 0. F1() by ; :: thesis: verum
end;
end;
end;
hence Aa * (i,(f9 /. i)) <> 0. F1() ; :: thesis: ( ( j in dom f9 & i < j implies f9 /. i < f9 /. j ) & ( j in (dom f9) \ {i} implies Aa * (j,(f9 /. i)) = 0. F1() ) & ( j in Seg (width Aa) & j < f9 /. i implies Aa * (i,j) = 0. F1() ) )
thus ( j in dom f9 & i < j implies f9 /. i < f9 /. j ) :: thesis: ( ( j in (dom f9) \ {i} implies Aa * (j,(f9 /. i)) = 0. F1() ) & ( j in Seg (width Aa) & j < f9 /. i implies Aa * (i,j) = 0. F1() ) )
proof
assume that
A141: j in dom f9 and
A142: i < j ; :: thesis: f9 /. i < f9 /. j
per cases ( ( j in {((len f) + 1)} & i in {((len f) + 1)} ) or ( j in {((len f) + 1)} & i in dom f ) or ( j in dom f & i in {((len f) + 1)} ) or ( j in dom f & i in dom f ) ) by ;
suppose A143: ( j in {((len f) + 1)} & i in {((len f) + 1)} ) ; :: thesis: f9 /. i < f9 /. j
then i = (len f) + 1 by TARSKI:def 1;
hence f9 /. i < f9 /. j by ; :: thesis: verum
end;
suppose A144: ( j in {((len f) + 1)} & i in dom f ) ; :: thesis: f9 /. i < f9 /. j
then (len f) + 1 = j by TARSKI:def 1;
then A145: f9 . j = n + 1 by FINSEQ_1:42;
( f /. i = f . i & f . i in rng f ) by ;
then A146: f /. i <= n by ;
f9 . j = f9 /. j by ;
then f /. i < f9 /. j by ;
hence f9 /. i < f9 /. j by ; :: thesis: verum
end;
suppose ( j in dom f & i in {((len f) + 1)} ) ; :: thesis: f9 /. i < f9 /. j
then ( j <= len f & i = (len f) + 1 ) by ;
hence f9 /. i < f9 /. j by ; :: thesis: verum
end;
suppose A147: ( j in dom f & i in dom f ) ; :: thesis: f9 /. i < f9 /. j
then ( f /. i = f9 /. i & f /. j = f9 /. j ) by A135;
hence f9 /. i < f9 /. j by ; :: thesis: verum
end;
end;
end;
dom f9 = Seg (len f9) by FINSEQ_1:def 3;
then A148: dom f9 c= dom Aa by ;
thus ( j in (dom f9) \ {i} implies Aa * (j,(f9 /. i)) = 0. F1() ) :: thesis: ( j in Seg (width Aa) & j < f9 /. i implies Aa * (i,j) = 0. F1() )
proof
assume A149: j in (dom f9) \ {i} ; :: thesis: Aa * (j,(f9 /. i)) = 0. F1()
per cases ( i = (len f) + 1 or i <> (len f) + 1 ) ;
suppose A150: i = (len f) + 1 ; :: thesis: Aa * (j,(f9 /. i)) = 0. F1()
(len f) + 1 in {((len f) + 1)} by TARSKI:def 1;
then (len f) + 1 in dom f9 by ;
then A151: f9 . ((len f) + 1) = f9 /. i by ;
A152: j in dom f9 by ;
j <> i by ;
then A153: j in (dom Aa) \ {i} by ;
j <= F2() by ;
then Aa * (j,(n + 1)) = 0. F1() by ;
hence Aa * (j,(f9 /. i)) = 0. F1() by ; :: thesis: verum
end;
suppose A154: i <> (len f) + 1 ; :: thesis: Aa * (j,(f9 /. i)) = 0. F1()
A155: j in dom f9 by ;
A156: ( i in dom f or i in {((len f) + 1)} ) by ;
then A157: f . i in rng f by ;
A158: ( f /. i = f9 /. i & f . i = f /. i ) by ;
then A159: 1 <= f9 /. i by ;
A160: f9 /. i <= n by ;
n <= F3() by ;
then f9 /. i <= F3() by ;
then f9 /. i in Seg (width Aa) by ;
then A161: [j,(f9 /. i)] in Indices Aa by ;
per cases ( j = (len f) + 1 or j <> (len f) + 1 ) ;
suppose j = (len f) + 1 ; :: thesis: Aa * (j,(f9 /. i)) = 0. F1()
then j > len f by NAT_1:13;
hence Aa * (j,(f9 /. i)) = 0. F1() by ; :: thesis: verum
end;
suppose A162: j <> (len f) + 1 ; :: thesis: Aa * (j,(f9 /. i)) = 0. F1()
j in dom f9 by ;
then A163: ( j in dom f or j in {((len f) + 1)} ) by ;
j <> i by ;
then j in (dom f) \ {i} by ;
then Aa * (j,(f /. i)) = 0. F1() by ;
hence Aa * (j,(f9 /. i)) = 0. F1() by ; :: thesis: verum
end;
end;
end;
end;
end;
thus ( j in Seg (width Aa) & j < f9 /. i implies Aa * (i,j) = 0. F1() ) :: thesis: verum
proof
assume that
A164: j in Seg (width Aa) and
A165: j < f9 /. i ; :: thesis: Aa * (i,j) = 0. F1()
per cases ( i in dom f or not i in dom f ) ;
suppose A166: i in dom f ; :: thesis: Aa * (i,j) = 0. F1()
then f9 /. i = f /. i by A135;
hence Aa * (i,j) = 0. F1() by ; :: thesis: verum
end;
suppose A167: not i in dom f ; :: thesis: Aa * (i,j) = 0. F1()
( i in dom f or i in {((len f) + 1)} ) by ;
then A168: i = (len f) + 1 by ;
then A169: f9 . i = n + 1 by FINSEQ_1:42;
f9 . i = f9 /. i by ;
then A170: j <= n by ;
A171: i > len f by ;
[i,j] in Indices Aa by ;
hence Aa * (i,j) = 0. F1() by ; :: thesis: verum
end;
end;
end;
end;
A172: ( rng <*(n + 1)*> = {(n + 1)} & (rng f) \/ {(n + 1)} c= (Seg n) \/ {(n + 1)} ) by ;
A173: (Seg n) \/ {(n + 1)} = Seg (n + 1) by FINSEQ_1:9;
( rng f misses {(n + 1)} & <*(n + 1)*> is one-to-one ) by ;
hence ( ( for i, j being Nat st [i,j] in Indices Aa & i > len f9 & j <= n + 1 holds
Aa * (i,j) = 0. F1() ) & f9 is one-to-one & len f9 <= n + 1 & len f9 <= F2() & rng f9 c= Seg (n + 1) & ( for i, j being Nat st i in dom f9 holds
S1[f9,i,j,Aa] ) ) by ; :: thesis: verum
end;
end;
end;
A174: S2[ 0 ]
proof
assume 0 <= F3() ; :: thesis: ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= 0 holds
A9 * (i,j) = 0. F1() ) & f is one-to-one & len f <= 0 & len f <= F2() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )

take A9 = F5(); :: thesis: ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= 0 holds
A9 * (i,j) = 0. F1() ) & f is one-to-one & len f <= 0 & len f <= F2() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )

take B9 = F6(); :: thesis: ( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= 0 holds
A9 * (i,j) = 0. F1() ) & f is one-to-one & len f <= 0 & len f <= F2() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )

thus ( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 ) by A1; :: thesis: ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= 0 holds
A9 * (i,j) = 0. F1() ) & f is one-to-one & len f <= 0 & len f <= F2() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) )

take f = <*> NAT; :: thesis: ( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= 0 holds
A9 * (i,j) = 0. F1() ) & f is one-to-one & len f <= 0 & len f <= F2() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) )

now :: thesis: for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= 0 holds
A9 * (i,j) = 0. F1()
let i, j be Nat; :: thesis: ( [i,j] in Indices A9 & i > len f & j <= 0 implies A9 * (i,j) = 0. F1() )
assume that
A175: [i,j] in Indices A9 and
i > len f and
A176: j <= 0 ; :: thesis: A9 * (i,j) = 0. F1()
j in Seg (width A9) by ;
hence A9 * (i,j) = 0. F1() by A176; :: thesis: verum
end;
hence ( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= 0 holds
A9 * (i,j) = 0. F1() ) & f is one-to-one & len f <= 0 & len f <= F2() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) ; :: thesis: verum
end;
for n being Nat holds S2[n] from then consider A9 being Matrix of F2(),F3(),F1(), B9 being Matrix of F2(),F4(),F1() such that
A177: P1[A9,B9] and
A178: the_rank_of F5() = the_rank_of A9 and
A179: ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= F3() holds
A9 * (i,j) = 0. F1() ) & f is one-to-one & len f <= F3() & len f <= F2() & rng f c= Seg F3() & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) ;
consider f being FinSequence of NAT such that
A180: for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= F3() holds
A9 * (i,j) = 0. F1() and
A181: f is one-to-one and
len f <= F3() and
A182: len f <= F2() and
A183: rng f c= Seg F3() and
A184: for i, j being Nat st i in dom f holds
S1[f,i,j,A9] by A179;
A185: len A9 = F2() by ;
take A9 ; :: thesis: ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ( for i being Nat st i in dom A9 & i > the_rank_of F5() holds
Line (A9,i) = F3() |-> (0. F1()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A9 & f is one-to-one & rng f c= Seg (width A9) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )

take B9 ; :: thesis: ( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ( for i being Nat st i in dom A9 & i > the_rank_of F5() holds
Line (A9,i) = F3() |-> (0. F1()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A9 & f is one-to-one & rng f c= Seg (width A9) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )

thus ( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 ) by ; :: thesis: ( ( for i being Nat st i in dom A9 & i > the_rank_of F5() holds
Line (A9,i) = F3() |-> (0. F1()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A9 & f is one-to-one & rng f c= Seg (width A9) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )

A186: dom A9 = Seg (len A9) by FINSEQ_1:def 3;
set L = len f;
A187: Seg (len f) c= Seg F2() by ;
( idseq (len f) is FinSequence of NAT & len (idseq (len f)) = len f ) by ;
then reconsider idL = idseq (len f), F9 = f as Element of (len f) -tuples_on NAT by FINSEQ_2:92;
set S = Segm (A9,idL,F9);
A188: dom f = Seg (len f) by FINSEQ_1:def 3;
set D = diagonal_of_Matrix (Segm (A9,idL,F9));
A189: Indices (Segm (A9,idL,F9)) = [:(Seg (len f)),(Seg (len f)):] by MATRIX_0:24;
for k being Nat st k in dom (diagonal_of_Matrix (Segm (A9,idL,F9))) holds
(diagonal_of_Matrix (Segm (A9,idL,F9))) . k <> 0. F1()
proof
A190: len (diagonal_of_Matrix (Segm (A9,idL,F9))) = len f by MATRIX_3:def 10;
let k be Nat; :: thesis: ( k in dom (diagonal_of_Matrix (Segm (A9,idL,F9))) implies (diagonal_of_Matrix (Segm (A9,idL,F9))) . k <> 0. F1() )
assume k in dom (diagonal_of_Matrix (Segm (A9,idL,F9))) ; :: thesis: (diagonal_of_Matrix (Segm (A9,idL,F9))) . k <> 0. F1()
then A191: k in Seg (len f) by ;
then [k,k] in Indices (Segm (A9,idL,F9)) by ;
then (Segm (A9,idL,F9)) * (k,k) = A9 * ((idL . k),(f . k)) by MATRIX13:def 1
.= A9 * (k,(f . k)) by
.= A9 * (k,(f /. k)) by ;
then (Segm (A9,idL,F9)) * (k,k) <> 0. F1() by ;
hence (diagonal_of_Matrix (Segm (A9,idL,F9))) . k <> 0. F1() by ; :: thesis: verum
end;
then A192: Product (diagonal_of_Matrix (Segm (A9,idL,F9))) <> 0. F1() by FVSUM_1:82;
now :: thesis: for i, j being Nat st [i,j] in Indices (Segm (A9,idL,F9)) & i > j holds
(Segm (A9,idL,F9)) * (i,j) = 0. F1()
let i, j be Nat; :: thesis: ( [i,j] in Indices (Segm (A9,idL,F9)) & i > j implies (Segm (A9,idL,F9)) * (i,j) = 0. F1() )
assume A193: [i,j] in Indices (Segm (A9,idL,F9)) ; :: thesis: ( i > j implies (Segm (A9,idL,F9)) * (i,j) = 0. F1() )
A194: i in Seg (len f) by ;
assume i > j ; :: thesis: (Segm (A9,idL,F9)) * (i,j) = 0. F1()
then A195: i in (dom f) \ {j} by ;
reconsider i9 = i, j9 = j as Element of NAT by ORDINAL1:def 12;
A196: j in Seg (len f) by ;
thus (Segm (A9,idL,F9)) * (i,j) = A9 * ((idL . i9),(f . j9)) by
.= A9 * (i,(f . j)) by
.= A9 * (i,(f /. j)) by
.= 0. F1() by ; :: thesis: verum
end;
then Segm (A9,idL,F9) is upper_triangular Matrix of len f,F1() by MATRIX_1:def 8;
then A197: Det (Segm (A9,idL,F9)) <> 0. F1() by ;
A198: len (Segm (A9,(Seg (len f)),(Seg (width A9)))) = card (Seg (len f)) by MATRIX_0:def 2;
A199: width A9 = F3() by ;
[:(rng idL),(rng F9):] c= Indices A9 by ;
then A200: the_rank_of A9 >= len f by ;
A201: now :: thesis: for i being Nat st i in (dom A9) \ (Seg (len f)) holds
Line (A9,i) = (width A9) |-> (0. F1())
set w0 = (width A9) |-> (0. F1());
let i be Nat; :: thesis: ( i in (dom A9) \ (Seg (len f)) implies Line (A9,i) = (width A9) |-> (0. F1()) )
assume A202: i in (dom A9) \ (Seg (len f)) ; :: thesis: Line (A9,i) = (width A9) |-> (0. F1())
set LA = Line (A9,i);
A203: now :: thesis: for j being Nat st 1 <= j & j <= width A9 holds
(Line (A9,i)) . j = ((width A9) |-> (0. F1())) . j
not i in Seg (len f) by ;
then A204: ( i > len f or i < 1 ) ;
let j be Nat; :: thesis: ( 1 <= j & j <= width A9 implies (Line (A9,i)) . j = ((width A9) |-> (0. F1())) . j )
assume that
A205: 1 <= j and
A206: j <= width A9 ; :: thesis: (Line (A9,i)) . j = ((width A9) |-> (0. F1())) . j
A207: j in Seg (width A9) by ;
A208: i in dom A9 by ;
then A209: [i,j] in Indices A9 by ;
thus (Line (A9,i)) . j = A9 * (i,j) by
.= 0. F1() by
.= ((width A9) |-> (0. F1())) . j by ; :: thesis: verum
end;
( len (Line (A9,i)) = width A9 & len ((width A9) |-> (0. F1())) = width A9 ) by CARD_1:def 7;
hence Line (A9,i) = (width A9) |-> (0. F1()) by A203; :: thesis: verum
end;
then the_rank_of A9 = the_rank_of (Segm (A9,(Seg (len f)),(Seg (width A9)))) by ;
then the_rank_of A9 <= card (Seg (len f)) by ;
then A210: the_rank_of A9 <= len f by FINSEQ_1:57;
then A211: the_rank_of F5() = len f by ;
thus for i being Nat st i in dom A9 & i > the_rank_of F5() holds
Line (A9,i) = F3() |-> (0. F1()) :: thesis: ex f being FinSequence of NAT st
( len f = the_rank_of A9 & f is one-to-one & rng f c= Seg (width A9) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) )
proof
let i be Nat; :: thesis: ( i in dom A9 & i > the_rank_of F5() implies Line (A9,i) = F3() |-> (0. F1()) )
assume that
A212: i in dom A9 and
A213: i > the_rank_of F5() ; :: thesis: Line (A9,i) = F3() |-> (0. F1())
not i in Seg (len f) by ;
then i in (dom A9) \ (Seg (len f)) by ;
hence Line (A9,i) = F3() |-> (0. F1()) by ; :: thesis: verum
end;
take f ; :: thesis: ( len f = the_rank_of A9 & f is one-to-one & rng f c= Seg (width A9) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) )

thus ( len f = the_rank_of A9 & f is one-to-one & rng f c= Seg (width A9) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) by ; :: thesis: verum
end;
end;
end;
then consider A9 being Matrix of F2(),F3(),F1(), B9 being Matrix of F2(),F4(),F1() such that
A214: P1[A9,B9] and
A215: the_rank_of F5() = the_rank_of A9 and
A216: for i being Nat st i in dom A9 & i > the_rank_of F5() holds
Line (A9,i) = F3() |-> (0. F1()) and
A217: ex f being FinSequence of NAT st
( len f = the_rank_of A9 & f is one-to-one & rng f c= Seg (width A9) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) ;
consider f being FinSequence of NAT such that
A218: len f = the_rank_of A9 and
A219: f is one-to-one and
A220: rng f c= Seg (width A9) and
A221: for i, j being Nat st i in dom f holds
S1[f,i,j,A9] by A217;
not 0 in rng f by A220;
then reconsider rngf = rng f as finite without_zero Subset of NAT by ;
A222: ( F2() = 0 or F2() > 0 ) ;
set S = Segm (A9,(Seg (card rngf)),rngf);
A223: dom f = Seg (the_rank_of F5()) by ;
take A9 ; :: thesis: ex B9 being Matrix of F2(),F4(),F1() ex N being finite without_zero Subset of NAT st
( N c= Seg F3() & the_rank_of F5() = the_rank_of A9 & the_rank_of F5() = card N & P1[A9,B9] & Segm (A9,(Seg (card N)),N) is diagonal & ( for i being Nat st i in Seg (card N) holds
A9 * (i,((Sgm N) /. i)) <> 0. F1() ) & ( for i being Nat st i in dom A9 & i > card N holds
Line (A9,i) = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width A9) & j < (Sgm N) . i holds
A9 * (i,j) = 0. F1() ) )

take B9 ; :: thesis: ex N being finite without_zero Subset of NAT st
( N c= Seg F3() & the_rank_of F5() = the_rank_of A9 & the_rank_of F5() = card N & P1[A9,B9] & Segm (A9,(Seg (card N)),N) is diagonal & ( for i being Nat st i in Seg (card N) holds
A9 * (i,((Sgm N) /. i)) <> 0. F1() ) & ( for i being Nat st i in dom A9 & i > card N holds
Line (A9,i) = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width A9) & j < (Sgm N) . i holds
A9 * (i,j) = 0. F1() ) )

take rngf ; :: thesis: ( rngf c= Seg F3() & the_rank_of F5() = the_rank_of A9 & the_rank_of F5() = card rngf & P1[A9,B9] & Segm (A9,(Seg (card rngf)),rngf) is diagonal & ( for i being Nat st i in Seg (card rngf) holds
A9 * (i,((Sgm rngf) /. i)) <> 0. F1() ) & ( for i being Nat st i in dom A9 & i > card rngf holds
Line (A9,i) = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card rngf) & j in Seg (width A9) & j < (Sgm rngf) . i holds
A9 * (i,j) = 0. F1() ) )

len A9 = F2() by MATRIX_0:def 2;
then ( width A9 = 0 or width A9 = F3() ) by ;
then Seg (width A9) c= Seg F3() ;
hence ( rngf c= Seg F3() & the_rank_of F5() = the_rank_of A9 ) by ; :: thesis: ( the_rank_of F5() = card rngf & P1[A9,B9] & Segm (A9,(Seg (card rngf)),rngf) is diagonal & ( for i being Nat st i in Seg (card rngf) holds
A9 * (i,((Sgm rngf) /. i)) <> 0. F1() ) & ( for i being Nat st i in dom A9 & i > card rngf holds
Line (A9,i) = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card rngf) & j in Seg (width A9) & j < (Sgm rngf) . i holds
A9 * (i,j) = 0. F1() ) )

dom f,rngf are_equipotent by ;
hence A224: card rngf = card (dom f) by CARD_1:5
.= card (Seg (the_rank_of F5())) by
.= the_rank_of F5() by FINSEQ_1:57 ;
:: thesis: ( P1[A9,B9] & Segm (A9,(Seg (card rngf)),rngf) is diagonal & ( for i being Nat st i in Seg (card rngf) holds
A9 * (i,((Sgm rngf) /. i)) <> 0. F1() ) & ( for i being Nat st i in dom A9 & i > card rngf holds
Line (A9,i) = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card rngf) & j in Seg (width A9) & j < (Sgm rngf) . i holds
A9 * (i,j) = 0. F1() ) )

now :: thesis: for i, j being Nat st i in dom f & j in dom f & i < j holds
f . i < f . j
let i, j be Nat; :: thesis: ( i in dom f & j in dom f & i < j implies f . i < f . j )
assume that
A225: ( i in dom f & j in dom f ) and
A226: i < j ; :: thesis: f . i < f . j
( f . i = f /. i & f . j = f /. j ) by ;
hence f . i < f . j by ; :: thesis: verum
end;
then A227: Sgm rngf = f by ;
thus P1[A9,B9] by A214; :: thesis: ( Segm (A9,(Seg (card rngf)),rngf) is diagonal & ( for i being Nat st i in Seg (card rngf) holds
A9 * (i,((Sgm rngf) /. i)) <> 0. F1() ) & ( for i being Nat st i in dom A9 & i > card rngf holds
Line (A9,i) = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card rngf) & j in Seg (width A9) & j < (Sgm rngf) . i holds
A9 * (i,j) = 0. F1() ) )

A228: card (Seg (card rngf)) = card rngf by FINSEQ_1:57;
then A229: Indices (Segm (A9,(Seg (card rngf)),rngf)) = [:(Seg (the_rank_of F5())),(Seg (the_rank_of F5())):] by ;
now :: thesis: for i, j being Nat st i in Seg (the_rank_of F5()) & j in Seg (the_rank_of F5()) & i <> j holds
(Segm (A9,(Seg (card rngf)),rngf)) * (i,j) = 0. F1()
let i, j be Nat; :: thesis: ( i in Seg (the_rank_of F5()) & j in Seg (the_rank_of F5()) & i <> j implies (Segm (A9,(Seg (card rngf)),rngf)) * (i,j) = 0. F1() )
assume that
A230: i in Seg (the_rank_of F5()) and
A231: j in Seg (the_rank_of F5()) and
A232: i <> j ; :: thesis: (Segm (A9,(Seg (card rngf)),rngf)) * (i,j) = 0. F1()
A233: i in (dom f) \ {j} by ;
A234: (idseq (the_rank_of F5())) . i = i by ;
[i,j] in Indices (Segm (A9,(Seg (card rngf)),rngf)) by ;
then (Segm (A9,(Seg (card rngf)),rngf)) * (i,j) = A9 * (((Sgm (Seg (the_rank_of F5()))) . i),(f . j)) by
.= A9 * (i,(f . j)) by
.= A9 * (i,(f /. j)) by ;
hence (Segm (A9,(Seg (card rngf)),rngf)) * (i,j) = 0. F1() by ; :: thesis: verum
end;
hence Segm (A9,(Seg (card rngf)),rngf) is diagonal by ; :: thesis: ( ( for i being Nat st i in Seg (card rngf) holds
A9 * (i,((Sgm rngf) /. i)) <> 0. F1() ) & ( for i being Nat st i in dom A9 & i > card rngf holds
Line (A9,i) = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card rngf) & j in Seg (width A9) & j < (Sgm rngf) . i holds
A9 * (i,j) = 0. F1() ) )

thus for i being Nat st i in Seg (card rngf) holds
A9 * (i,((Sgm rngf) /. i)) <> 0. F1() by ; :: thesis: ( ( for i being Nat st i in dom A9 & i > card rngf holds
Line (A9,i) = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card rngf) & j in Seg (width A9) & j < (Sgm rngf) . i holds
A9 * (i,j) = 0. F1() ) )

thus for i being Nat st i in dom A9 & i > card rngf holds
Line (A9,i) = F3() |-> (0. F1()) by ; :: thesis: for i, j being Nat st i in Seg (card rngf) & j in Seg (width A9) & j < (Sgm rngf) . i holds
A9 * (i,j) = 0. F1()

let i, j be Nat; :: thesis: ( i in Seg (card rngf) & j in Seg (width A9) & j < (Sgm rngf) . i implies A9 * (i,j) = 0. F1() )
assume that
A235: i in Seg (card rngf) and
A236: j in Seg (width A9) and
A237: j < (Sgm rngf) . i ; :: thesis: A9 * (i,j) = 0. F1()
j < f /. i by ;
hence A9 * (i,j) = 0. F1() by ; :: thesis: verum