defpred S₁[ FinSequence of NAT , Nat, Nat, Matrix of the carrier of F₁(),F₂(),] means ( $4 * $2,($1 /. $2) <> 0. F₁() & ( $3 in dom $1 & $2 < $3 implies $1 /. $2 < $1 /. $3 ) & ( $3 in (dom $1) \ {$2} implies $4 * $3,($1 /. $2) = 0. F₁() ) & ( $3 in Seg (width $4) & $3 < $1 /. $2 implies $4 * $2,$3 = 0. F₁() ) );
set r = the_rank_of F₅();
ex A' being Matrix of the carrier of F₁(),F₂(), ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & ( for i being Nat st i in dom A' & i > the_rank_of F₅() holds
Line A',i = F₃() |-> (0. F₁()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) ) )

proof

per cases ( F₂() = 0 or F₂() > 0 ) ;

suppose A3: F₂() = 0 ; :: thesis: ex A' being Matrix of the carrier of F₁(),F₂(), ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & ( for i being Nat st i in dom A' & i > the_rank_of F₅() holds
Line A',i = F₃() |-> (0. F₁()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) ) )

take A' = F₅(); :: thesis: ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & ( for i being Nat st i in dom A' & i > the_rank_of F₅() holds
Line A',i = F₃() |-> (0. F₁()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) ) )
take B' = F₆(); :: thesis: ( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & ( for i being Nat st i in dom A' & i > the_rank_of F₅() holds
Line A',i = F₃() |-> (0. F₁()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) ) )
( dom A' = Seg (len A') & len A' = 0 ) by A3, FINSEQ_1:def 3, MATRIX_1:def 3;
hence ( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & ( for i being Nat st i in dom A' & i > the_rank_of F₅() holds
Line A',i = F₃() |-> (0. F₁()) ) ) by A1; :: thesis: ex f being FinSequence of NAT st
( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) )
take f = <*> NAT ; :: thesis: ( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) )
len A' = 0 by A3, MATRIX_1:23;
hence ( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) ) by MATRIX13:74, XBOOLE_1:2; :: thesis: verum

end;

suppose A4: F₂() > 0 ; :: thesis: ex A' being Matrix of the carrier of F₁(),F₂(), ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & ( for i being Nat st i in dom A' & i > the_rank_of F₅() holds
Line A',i = F₃() |-> (0. F₁()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) ) )

defpred S₂[ Nat] means ( $1 <= F₃() implies ex A' being Matrix of the carrier of F₁(),F₂(), ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= $1 holds
A' * i,j = 0. F₁() ) & f is one-to-one & len f <= $1 & len f <= F₂() & rng f c= Seg $1 & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) ) ) );
A5: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A6: S₂[n] ; :: thesis: S₂[n + 1]
set n1 = n + 1;
assume A7: n + 1 <= F₃() ; :: thesis: ex A' being Matrix of the carrier of F₁(),F₂(), ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n + 1 holds
A' * i,j = 0. F₁() ) & f is one-to-one & len f <= n + 1 & len f <= F₂() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) ) )
then consider A' being Matrix of the carrier of F₁(),F₂(),, B' being Matrix of the carrier of F₁(),F₂(), such that
A8: ( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' ) and
A9: ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F₁() ) & f is one-to-one & len f <= n & len f <= F₂() & rng f c= Seg n & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) ) by A6, NAT_1:13;
consider f being FinSequence of NAT such that
A10: for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F₁() and
A11: f is one-to-one and
A12: len f <= n and
A13: len f <= F₂() and
A14: rng f c= Seg n and
A15: for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] by A9;

per cases ( for i, j being Nat st [i,j] in Indices A' & i > len f & j = n + 1 holds
A' * i,j = 0. F₁() or ex i, j being Nat st
( [i,j] in Indices A' & i > len f & j = n + 1 & A' * i,j <> 0. F₁() ) ) ;

suppose A16: for i, j being Nat st [i,j] in Indices A' & i > len f & j = n + 1 holds
A' * i,j = 0. F₁() ; :: thesis: ex A' being Matrix of the carrier of F₁(),F₂(), ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n + 1 holds
A' * i,j = 0. F₁() ) & f is one-to-one & len f <= n + 1 & len f <= F₂() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) ) )

A17: now

let i, j be Nat; :: thesis: ( [i,j] in Indices A' & i > len f & j <= n + 1 implies A' * i,j = 0. F₁() )
assume that
A18: ( [i,j] in Indices A' & i > len f ) and
A19: j <= n + 1 ; :: thesis: A' * i,j = 0. F₁()
( j <= n or j = n + 1 ) by A19, NAT_1:8;
hence A' * i,j = 0. F₁() by A10, A16, A18; :: thesis: verum

end;

n <= n + 1 by NAT_1:13;
then Seg n c= Seg (n + 1) by FINSEQ_1:7;
then A20: rng f c= Seg (n + 1) by A14, XBOOLE_1:1;
len f <= n + 1 by A12, NAT_1:12;
hence ex A' being Matrix of the carrier of F₁(),F₂(), ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n + 1 holds
A' * i,j = 0. F₁() ) & f is one-to-one & len f <= n + 1 & len f <= F₂() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) ) ) by A8, A11, A13, A15, A17, A20; :: thesis: verum

end;

suppose ex i, j being Nat st
( [i,j] in Indices A' & i > len f & j = n + 1 & A' * i,j <> 0. F₁() ) ; :: thesis: ex A' being Matrix of the carrier of F₁(),F₂(), ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n + 1 holds
A' * i,j = 0. F₁() ) & f is one-to-one & len f <= n + 1 & len f <= F₂() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) ) )

then consider i0, j0 being Nat such that
A21: [i0,j0] in Indices A' and
A22: i0 > len f and
A23: j0 = n + 1 and
A24: A' * i0,j0 <> 0. F₁() ;
A25: Indices A' = [:(Seg F₂()),(Seg F₃()):] by A4, MATRIX_1:24;
then A26: n + 1 in Seg F₃() by A21, A23, ZFMISC_1:106;
A27: i0 in Seg F₂() by A21, A25, ZFMISC_1:106;
then A28: i0 <= F₂() by FINSEQ_1:3;
A29: (len f) + 1 <= i0 by A22, NAT_1:13;
then ( 0 + 1 <= (len f) + 1 & (len f) + 1 <= F₂() ) by A28, XREAL_1:9, XXREAL_0:2;
then A30: (len f) + 1 in Seg F₂() ;
defpred S₃[ Nat] means ( $1 <= F₂() implies ex A' being Matrix of the carrier of F₁(),F₂(), ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F₁() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F₁() ) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) & ( for j being Nat st j in (dom A') \ {((len f) + 1)} & j <= $1 holds
A' * j,(n + 1) = 0. F₁() ) ) );
A31: dom f = Seg (len f) by FINSEQ_1:def 3;
n <= F₃() by A7, NAT_1:13;
then A32: Seg n c= Seg F₃() by FINSEQ_1:7;
A33: Seg (len f) c= Seg F₂() by A13, FINSEQ_1:7;
A34: for k being Nat st S₃[k] holds
S₃[k + 1]

proof

let k be Nat; :: thesis: ( S₃[k] implies S₃[k + 1] )
assume A35: S₃[k] ; :: thesis: S₃[k + 1]
set k1 = k + 1;
assume k + 1 <= F₂() ; :: thesis: ex A' being Matrix of the carrier of F₁(),F₂(), ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F₁() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F₁() ) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) & ( for j being Nat st j in (dom A') \ {((len f) + 1)} & j <= k + 1 holds
A' * j,(n + 1) = 0. F₁() ) )
then consider AA being Matrix of the carrier of F₁(),F₂(),, BB being Matrix of the carrier of F₁(),F₂(), such that
A36: P₁[AA,BB] and
A37: the_rank_of F₅() = the_rank_of AA and
A38: AA * ((len f) + 1),(n + 1) <> 0. F₁() and
A39: for i, j being Nat st [i,j] in Indices AA & i > len f & j <= n holds
AA * i,j = 0. F₁() and
A40: for i, j being Nat st i in dom f holds
S₁[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. F₁() by A35, NAT_1:13;

now

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 the carrier of F₁(),F₂(), ex RB being Matrix of the carrier of F₁(),F₂(), ex A' being Matrix of the carrier of F₁(),F₂(), ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F₁() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F₁() ) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) & ( for j being Nat st j in (dom A') \ {((len f) + 1)} & j <= k + 1 holds
A' * j,(n + 1) = 0. F₁() ) )

take RA = AA; :: thesis: ex RB being Matrix of the carrier of F₁(),F₂(), ex A' being Matrix of the carrier of F₁(),F₂(), ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F₁() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F₁() ) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) & ( for j being Nat st j in (dom A') \ {((len f) + 1)} & j <= k + 1 holds
A' * j,(n + 1) = 0. F₁() ) )
take RB = BB; :: thesis: ex A' being Matrix of the carrier of F₁(),F₂(), ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F₁() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F₁() ) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) & ( for j being Nat st j in (dom A') \ {((len f) + 1)} & j <= k + 1 holds
A' * j,(n + 1) = 0. F₁() ) )

now

let j be Nat; :: thesis: ( j in (dom RA) \ {((len f) + 1)} & j <= k + 1 implies RA * j,(n + 1) = 0. F₁() )
assume that
A43: j in (dom RA) \ {((len f) + 1)} and
A44: j <= k + 1 ; :: thesis: RA * j,(n + 1) = 0. F₁()
j <> (len f) + 1 by A43, ZFMISC_1:64;
then j < k + 1 by A42, A44, XXREAL_0:1;
then j <= k by NAT_1:13;
hence RA * j,(n + 1) = 0. F₁() by A41, A43; :: thesis: verum

end;

hence ex A' being Matrix of the carrier of F₁(),F₂(), ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F₁() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F₁() ) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) & ( for j being Nat st j in (dom A') \ {((len f) + 1)} & j <= k + 1 holds
A' * j,(n + 1) = 0. F₁() ) ) by A36, A37, A38, A39, A40; :: thesis: verum

end;

suppose A45: k + 1 <> (len f) + 1 ; :: thesis: ex RA being Matrix of F₂(),F₃(),the carrier of F₁() ex RB being Matrix of the carrier of F₁(),F₂(), ex A' being Matrix of the carrier of F₁(),F₂(), ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F₁() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F₁() ) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) & ( for j being Nat st j in (dom A') \ {((len f) + 1)} & j <= k + 1 holds
A' * j,(n + 1) = 0. F₁() ) )

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 = F₃() by A4, MATRIX_1:24;
then A47: len ((Line AA,(k + 1)) + ((- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (Line AA,((len f) + 1)))) = F₃() by FINSEQ_1:def 18;
A48: Indices A' = Indices AA by MATRIX_1:27;
then [((len f) + 1),(n + 1)] in Indices AA by A25, A30, A26, ZFMISC_1:106;
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. F₁() by A38, A45, A46, A47, MATRIX11:def 3;
A50: Indices A' = 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_1:27;

A51: now

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. F₁() )
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. F₁()

now

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. F₁()

A56: j in Seg F₃() by A25, A50, A52, ZFMISC_1:106;
then ( (len f) + 1 > len f & [((len f) + 1),j] in Indices A' ) by A25, A30, NAT_1:13, ZFMISC_1:106;
then AA * ((len f) + 1),j = 0. F₁() by A39, A48, A54;
then (Line AA,((len f) + 1)) . j = 0. F₁() by A46, A56, MATRIX_1:def 8;
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. F₁()) by A46, A56, FVSUM_1:63
.= 0. F₁() by VECTSP_1:36 ;
(Line AA,(k + 1)) . j = AA * (k + 1),j by A46, A56, MATRIX_1:def 8
.= 0. F₁() by A39, A48, A50, A52, A53, A54, A55 ;
then (0. F₁()) + (0. F₁()) = ((Line AA,(k + 1)) + ((- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (Line AA,((len f) + 1)))) . j by A46, A56, A57, FVSUM_1:22
.= (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 A48, A50, A46, A47, A52, A55, MATRIX11:def 3 ;
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. F₁() by RLVECT_1:def 7; :: 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. F₁()

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 A48, A50, A46, A47, A52, MATRIX11:def 3
.= 0. F₁() 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. F₁() ; :: thesis: verum

end;

set RB = F₇(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 the carrier of F₁(),F₂(), ex A' being Matrix of the carrier of F₁(),F₂(), ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F₁() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F₁() ) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) & ( for j being Nat st j in (dom A') \ {((len f) + 1)} & j <= k + 1 holds
A' * j,(n + 1) = 0. F₁() ) )
take RB = F₇(BB,(k + 1),((len f) + 1),(- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " )))); :: thesis: ex A' being Matrix of the carrier of F₁(),F₂(), ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F₁() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F₁() ) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) & ( for j being Nat st j in (dom A') \ {((len f) + 1)} & j <= k + 1 holds
A' * j,(n + 1) = 0. F₁() ) )
A58: width RA = F₃() by A4, MATRIX_1:24;
A59: len AA = F₂() by MATRIX_1:def 3;

A60: now

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. F₁() )
assume that
A62: j in (dom RA) \ {((len f) + 1)} and
A63: j <= k + 1 ; :: thesis: RA * j,(n + 1) = 0. F₁()
j in dom RA by A62, XBOOLE_0:def 5;
then A64: [j,(n + 1)] in Indices AA by A26, A48, A50, A58, ZFMISC_1:106;
A65: ( dom RA = Seg (len RA) & len RA = F₂() ) by FINSEQ_1:def 3, MATRIX_1:def 3;

now

per cases ( j <= k or j = k + 1 ) by A63, NAT_1:8;

suppose A66: j <= k ; :: thesis: RA * j,(n + 1) = 0. F₁()

then j < k + 1 by NAT_1:13;
hence RA * j,(n + 1) = AA * j,(n + 1) by A46, A47, A64, MATRIX11:def 3
.= 0. F₁() by A41, A59, A62, A65, A61, A66 ;
:: thesis: verum

end;

suppose A67: j = k + 1 ; :: thesis: RA * j,(n + 1) = 0. F₁()

(Line AA,((len f) + 1)) . (n + 1) = AA * ((len f) + 1),(n + 1) by A26, A46, MATRIX_1:def 8;
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 A26, A46, FVSUM_1:63
.= ((- (AA * (k + 1),(n + 1))) * ((AA * ((len f) + 1),(n + 1)) " )) * (AA * ((len f) + 1),(n + 1)) by VECTSP_1:41
.= (- (AA * (k + 1),(n + 1))) * (((AA * ((len f) + 1),(n + 1)) " ) * (AA * ((len f) + 1),(n + 1))) by GROUP_1:def 4
.= (- (AA * (k + 1),(n + 1))) * (1_ F₁()) by A38, VECTSP_1:def 22
.= - (AA * (k + 1),(n + 1)) by VECTSP_1:def 13 ;
(Line AA,(k + 1)) . (n + 1) = AA * (k + 1),(n + 1) by A26, A46, MATRIX_1:def 8;
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 A26, A46, A68, FVSUM_1:22
.= 0. F₁() by VECTSP_1:66 ;
hence RA * j,(n + 1) = 0. F₁() by A46, A47, A64, A67, MATRIX11:def 3; :: thesis: verum

end;

end;

end;

hence RA * j,(n + 1) = 0. F₁() ; :: thesis: verum

end;

A69: dom AA = Seg (len AA) by FINSEQ_1:def 3;

A70: now

let i, j be Nat; :: thesis: ( i in dom f implies ( RA * i,(f /. i) <> 0. F₁() & ( j in dom f & i < j implies f /. i < f /. j ) & ( j in (dom f) \ {i} implies RA * j,(f /. i) = 0. F₁() ) & ( j in Seg (width RA) & j < f /. i implies RA * i,j = 0. F₁() ) ) )
assume A71: i in dom f ; :: thesis: ( RA * i,(f /. i) <> 0. F₁() & ( j in dom f & i < j implies f /. i < f /. j ) & ( j in (dom f) \ {i} implies RA * j,(f /. i) = 0. F₁() ) & ( j in Seg (width RA) & j < f /. i implies RA * i,j = 0. F₁() ) )
set fi = f /. i;
A72: ( f /. i = f . i & f . i in rng f ) by A71, FUNCT_1:def 5, PARTFUN1:def 8;
then A73: f /. i in Seg n by A14;
A74: ( (len f) + 1 > len f & f /. i <= n ) by A14, A72, FINSEQ_1:3, NAT_1:13;
( [((len f) + 1),(f /. i)] in Indices AA & (Line AA,((len f) + 1)) . (f /. i) = AA * ((len f) + 1),(f /. i) ) by A25, A32, A30, A48, A46, A73, MATRIX_1:def 8, ZFMISC_1:106;
then (Line AA,((len f) + 1)) . (f /. i) = 0. F₁() by A39, A74;
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. F₁()) by A32, A46, A73, FVSUM_1:63
.= 0. F₁() by VECTSP_1:44 ;
(Line AA,(k + 1)) . (f /. i) = AA * (k + 1),(f /. i) by A32, A46, A73, MATRIX_1:def 8;
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. F₁()) by A32, A46, A73, A75, FVSUM_1:22
.= AA * (k + 1),(f /. i) by RLVECT_1:def 7 ;
A77: [i,(f /. i)] in Indices AA by A25, A32, A33, A31, A48, A71, A73, ZFMISC_1:106;

now

per cases ( i <> k + 1 or i = k + 1 ) ;

suppose i <> k + 1 ; :: thesis: RA * i,(f /. i) <> 0. F₁()

then RA * i,(f /. i) = AA * i,(f /. i) by A46, A47, A77, MATRIX11:def 3;
hence RA * i,(f /. i) <> 0. F₁() by A40, A71; :: thesis: verum

end;

suppose i = k + 1 ; :: thesis: RA * i,(f /. i) <> 0. F₁()

then RA * i,(f /. i) = AA * i,(f /. i) by A46, A47, A77, A76, MATRIX11:def 3;
hence RA * i,(f /. i) <> 0. F₁() by A40, A71; :: thesis: verum

end;

end;

end;

hence ( RA * i,(f /. i) <> 0. F₁() & ( j in dom f & i < j implies f /. i < f /. j ) ) by A15, A71; :: thesis: ( ( j in (dom f) \ {i} implies RA * j,(f /. i) = 0. F₁() ) & ( j in Seg (width RA) & j < f /. i implies RA * i,j = 0. F₁() ) )
thus ( j in (dom f) \ {i} implies RA * j,(f /. i) = 0. F₁() ) :: thesis: ( j in Seg (width RA) & j < f /. i implies RA * i,j = 0. F₁() )

proof

assume A78: j in (dom f) \ {i} ; :: thesis: RA * j,(f /. i) = 0. F₁()
then j in Seg (len f) by A31, XBOOLE_0:def 5;
then A79: [j,(f /. i)] in Indices AA by A25, A32, A33, A48, A73, ZFMISC_1:106;

per cases ( j <> k + 1 or j = k + 1 ) ;

suppose j <> k + 1 ; :: thesis: RA * j,(f /. i) = 0. F₁()

hence RA * j,(f /. i) = AA * j,(f /. i) by A46, A47, A79, MATRIX11:def 3
.= 0. F₁() by A40, A71, A78 ;
:: thesis: verum

end;

suppose A80: j = k + 1 ; :: thesis: RA * j,(f /. i) = 0. F₁()

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 A46, A47, A79, MATRIX11:def 3
.= 0. F₁() 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. F₁() ) :: thesis: verum

proof

assume that
A81: j in Seg (width RA) and
A82: j < f /. i ; :: thesis: RA * i,j = 0. F₁()
A83: [((len f) + 1),j] in Indices AA by A30, A59, A69, A46, A58, A81, ZFMISC_1:106;
A84: [i,j] in Indices AA by A33, A31, A59, A69, A46, A58, A71, A81, ZFMISC_1:106;

per cases ( i <> k + 1 or i = k + 1 ) ;

suppose i <> k + 1 ; :: thesis: RA * i,j = 0. F₁()

hence RA * i,j = AA * i,j by A46, A47, A84, MATRIX11:def 3
.= 0. F₁() by A40, A46, A58, A71, A81, A82 ;
:: thesis: verum

end;

suppose A85: i = k + 1 ; :: thesis: RA * i,j = 0. F₁()

f /. i <= n by A14, A72, FINSEQ_1:3;
then A86: j <= n by A82, XXREAL_0:2;
(len f) + 1 > len f by NAT_1:13;
then 0. F₁() = AA * ((len f) + 1),j by A39, A83, A86
.= (Line AA,((len f) + 1)) . j by A46, A58, A81, MATRIX_1:def 8 ;
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. F₁()) by A46, A58, A81, FVSUM_1:63
.= 0. F₁() by VECTSP_1:36 ;
(Line AA,(k + 1)) . j = AA * i,j by A46, A58, A81, A85, MATRIX_1:def 8
.= 0. F₁() 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. F₁()) + (0. F₁()) by A46, A58, A81, A87, FVSUM_1:22
.= 0. F₁() by RLVECT_1:def 7 ;
hence RA * i,j = 0. F₁() by A46, A47, A84, A85, MATRIX11:def 3; :: thesis: verum

end;

end;

end;

end;

A88: (len f) + 1 in Seg (len AA) by A4, A30, MATRIX_1:24;
then A89: the_rank_of F₅() = the_rank_of RA by A37, A45, MATRIX13:92;
P₁[RA,RB] by A2, A36, A45, A88, A69;
hence ex A' being Matrix of the carrier of F₁(),F₂(), ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F₁() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F₁() ) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) & ( for j being Nat st j in (dom A') \ {((len f) + 1)} & j <= k + 1 holds
A' * j,(n + 1) = 0. F₁() ) ) by A89, A49, A51, A70, A60; :: thesis: verum

end;

end;

end;

hence ex A' being Matrix of the carrier of F₁(),F₂(), ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F₁() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F₁() ) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) & ( for j being Nat st j in (dom A') \ {((len f) + 1)} & j <= k + 1 holds
A' * j,(n + 1) = 0. F₁() ) ) ; :: thesis: verum

end;

A90: j0 in Seg F₃() by A21, A25, ZFMISC_1:106;
ex A' being Matrix of the carrier of F₁(),F₂(), ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F₁() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F₁() ) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) )

proof

per cases ( A' * ((len f) + 1),(n + 1) <> 0. F₁() or A' * ((len f) + 1),(n + 1) = 0. F₁() ) ;

suppose A' * ((len f) + 1),(n + 1) <> 0. F₁() ; :: thesis: ex A' being Matrix of the carrier of F₁(),F₂(), ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F₁() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F₁() ) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) )

hence ex A' being Matrix of the carrier of F₁(),F₂(), ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F₁() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F₁() ) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) ) by A8, A10, A15; :: thesis: verum

end;

suppose A91: A' * ((len f) + 1),(n + 1) = 0. F₁() ; :: thesis: ex A' being Matrix of the carrier of F₁(),F₂(), ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F₁() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F₁() ) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) )

set RB = F₇(B',((len f) + 1),i0,(1_ F₁()));
set LA = Line A',i0;
set LAf = Line A',((len f) + 1);
set RA = RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)));
take RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0))) ; :: thesis: ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[ RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0))),B'] & the_rank_of F₅() = the_rank_of (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) & (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * ((len f) + 1),(n + 1) <> 0. F₁() & ( for i, j being Nat st [i,j] in Indices (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) & i > len f & j <= n holds
(RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * i,j = 0. F₁() ) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j, RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))] ) )
take F₇(B',((len f) + 1),i0,(1_ F₁())) ; :: thesis: ( P₁[ RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0))),F₇(B',((len f) + 1),i0,(1_ F₁()))] & the_rank_of F₅() = the_rank_of (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) & (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * ((len f) + 1),(n + 1) <> 0. F₁() & ( for i, j being Nat st [i,j] in Indices (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) & i > len f & j <= n holds
(RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * i,j = 0. F₁() ) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j, RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))] ) )
( i0 in dom A' & dom A' = Seg (len A') ) by A21, FINSEQ_1:def 3, ZFMISC_1:106;
hence ( P₁[ RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0))),F₇(B',((len f) + 1),i0,(1_ F₁()))] & the_rank_of F₅() = the_rank_of (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) ) by A2, A8, A23, A24, A91, MATRIX13:92; :: thesis: ( (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * ((len f) + 1),(n + 1) <> 0. F₁() & ( for i, j being Nat st [i,j] in Indices (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) & i > len f & j <= n holds
(RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * i,j = 0. F₁() ) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j, RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))] ) )
A92: ( (1_ F₁()) * (Line A',i0) = Line A',i0 & len ((Line A',((len f) + 1)) + (Line A',i0)) = width A' ) by FINSEQ_1:def 18, FVSUM_1:70;
[((len f) + 1),j0] in Indices A' by A25, A30, A90, ZFMISC_1:106;
then A93: (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * ((len f) + 1),(n + 1) = ((Line A',((len f) + 1)) + (Line A',i0)) . (n + 1) by A23, A92, MATRIX11:def 3;
A94: width A' = F₃() by A4, MATRIX_1:24;
then A95: (Line A',i0) . (n + 1) = A' * i0,(n + 1) by A23, A90, MATRIX_1:def 8;
(Line A',((len f) + 1)) . (n + 1) = 0. F₁() by A23, A90, A91, A94, MATRIX_1:def 8;
then (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * ((len f) + 1),(n + 1) = (0. F₁()) + (A' * i0,(n + 1)) by A26, A94, A93, A95, FVSUM_1:22
.= A' * i0,(n + 1) by RLVECT_1:def 7 ;
hence (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * ((len f) + 1),(n + 1) <> 0. F₁() by A23, A24; :: thesis: ( ( for i, j being Nat st [i,j] in Indices (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) & i > len f & j <= n holds
(RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * i,j = 0. F₁() ) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j, RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))] ) )
A96: Indices (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) = Indices A' by MATRIX_1:27;

now

let i, j be Nat; :: thesis: ( [i,j] in Indices (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) & i > len f & j <= n implies (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * i,j = 0. F₁() )
assume that
A97: [i,j] in Indices (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) and
A98: i > len f and
A99: j <= n ; :: thesis: (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * i,j = 0. F₁()
A100: j in Seg F₃() by A94, A96, A97, ZFMISC_1:106;
A101: i >= (len f) + 1 by A98, NAT_1:13;

now

per cases ( i > (len f) + 1 or i = (len f) + 1 ) by A101, XXREAL_0:1;

suppose i > (len f) + 1 ; :: thesis: (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * i,j = 0. F₁()

hence (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * i,j = A' * i,j by A92, A96, A97, MATRIX11:def 3
.= 0. F₁() by A10, A96, A97, A98, A99 ;
:: thesis: verum

end;

suppose A102: i = (len f) + 1 ; :: thesis: (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * i,j = 0. F₁()

A103: [i0,j] in Indices A' by A25, A27, A100, ZFMISC_1:106;
A104: ( (Line A',((len f) + 1)) . j = A' * ((len f) + 1),j & (Line A',i0) . j = A' * i0,j ) by A94, A100, MATRIX_1:def 8;
(RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * i,j = ((Line A',((len f) + 1)) + (Line A',i0)) . j by A92, A96, A97, A102, MATRIX11:def 3;
hence (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * i,j = (A' * ((len f) + 1),j) + (A' * i0,j) by A94, A100, A104, FVSUM_1:22
.= (0. F₁()) + (A' * i0,j) by A10, A96, A97, A98, A99, A102
.= (0. F₁()) + (0. F₁()) by A10, A22, A99, A103
.= 0. F₁() by RLVECT_1:def 7 ;
:: thesis: verum

end;

end;

end;

hence (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * i,j = 0. F₁() ; :: thesis: verum

end;

hence for i, j being Nat st [i,j] in Indices (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) & i > len f & j <= n holds
(RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * i,j = 0. F₁() ; :: thesis: for i, j being Nat st i in dom f holds
S₁[f,i,j, RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))]
let i, j be Nat; :: thesis: ( i in dom f implies S₁[f,i,j, RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))] )
assume A105: i in dom f ; :: thesis: S₁[f,i,j, RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))]
i <= len f by A31, A105, FINSEQ_1:3;
then A106: i < (len f) + 1 by NAT_1:13;
( f /. i = f . i & f . i in rng f ) by A105, FUNCT_1:def 5, PARTFUN1:def 8;
then A107: f /. i in Seg n by A14;
then [i,(f /. i)] in Indices A' by A25, A32, A33, A31, A105, ZFMISC_1:106;
then (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * i,(f /. i) = A' * i,(f /. i) by A92, A106, MATRIX11:def 3;
hence ( (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * i,(f /. i) <> 0. F₁() & ( j in dom f & i < j implies f /. i < f /. j ) ) by A15, A105; :: thesis: ( ( j in (dom f) \ {i} implies (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * j,(f /. i) = 0. F₁() ) & ( j in Seg (width (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0))))) & j < f /. i implies (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * i,j = 0. F₁() ) )
thus ( j in (dom f) \ {i} implies (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * j,(f /. i) = 0. F₁() ) :: thesis: ( j in Seg (width (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0))))) & j < f /. i implies (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * i,j = 0. F₁() )

proof

assume A108: j in (dom f) \ {i} ; :: thesis: (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * j,(f /. i) = 0. F₁()
then A109: j in dom f by XBOOLE_0:def 5;
then j <= len f by A31, FINSEQ_1:3;
then A110: j < (len f) + 1 by NAT_1:13;
[j,(f /. i)] in Indices A' by A25, A32, A33, A31, A107, A109, ZFMISC_1:106;
hence (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * j,(f /. i) = A' * j,(f /. i) by A92, A110, MATRIX11:def 3
.= 0. F₁() by A15, A105, A108 ;
:: thesis: verum

end;

assume that
A111: j in Seg (width (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0))))) and
A112: j < f /. i ; :: thesis: (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * i,j = 0. F₁()
A113: width (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) = width A' by A92, MATRIX11:def 3;
then [i,j] in Indices A' by A25, A33, A31, A94, A105, A111, ZFMISC_1:106;
hence (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F₁()) * (Line A',i0)))) * i,j = A' * i,j by A92, A106, MATRIX11:def 3
.= 0. F₁() by A15, A105, A111, A112, A113 ;
:: thesis: verum

end;

end;

end;

then consider A0 being Matrix of the carrier of F₁(),F₂(),, B0 being Matrix of the carrier of F₁(),F₂(), such that
A114: ( P₁[A0,B0] & the_rank_of F₅() = the_rank_of A0 & A0 * ((len f) + 1),(n + 1) <> 0. F₁() & ( for i, j being Nat st [i,j] in Indices A0 & i > len f & j <= n holds
A0 * i,j = 0. F₁() ) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A0] ) ) ;
A115: S₃[ 0 ]

proof

assume 0 <= F₂() ; :: thesis: ex A' being Matrix of the carrier of F₁(),F₂(), ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F₁() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F₁() ) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) & ( for j being Nat st j in (dom A') \ {((len f) + 1)} & j <= 0 holds
A' * j,(n + 1) = 0. F₁() ) )
take A0 ; :: thesis: ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A0,B'] & the_rank_of F₅() = the_rank_of A0 & A0 * ((len f) + 1),(n + 1) <> 0. F₁() & ( for i, j being Nat st [i,j] in Indices A0 & i > len f & j <= n holds
A0 * i,j = 0. F₁() ) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A0] ) & ( for j being Nat st j in (dom A0) \ {((len f) + 1)} & j <= 0 holds
A0 * j,(n + 1) = 0. F₁() ) )
take B0 ; :: thesis: ( P₁[A0,B0] & the_rank_of F₅() = the_rank_of A0 & A0 * ((len f) + 1),(n + 1) <> 0. F₁() & ( for i, j being Nat st [i,j] in Indices A0 & i > len f & j <= n holds
A0 * i,j = 0. F₁() ) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A0] ) & ( for j being Nat st j in (dom A0) \ {((len f) + 1)} & j <= 0 holds
A0 * j,(n + 1) = 0. F₁() ) )

now

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. F₁() )
assume ( j in (dom A0) \ {((len f) + 1)} & j <= 0 ) ; :: thesis: A0 * j,(n + 1) = 0. F₁()
hence A0 * j,(n + 1) = 0. F₁() by A116; :: thesis: verum

end;

hence ( P₁[A0,B0] & the_rank_of F₅() = the_rank_of A0 & A0 * ((len f) + 1),(n + 1) <> 0. F₁() & ( for i, j being Nat st [i,j] in Indices A0 & i > len f & j <= n holds
A0 * i,j = 0. F₁() ) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A0] ) & ( for j being Nat st j in (dom A0) \ {((len f) + 1)} & j <= 0 holds
A0 * j,(n + 1) = 0. F₁() ) ) by A114; :: thesis: verum

end;

for k being Nat holds S₃[k] from NAT_1:sch 2(A115, A34);
then consider Aa being Matrix of the carrier of F₁(),F₂(),, Bb being Matrix of the carrier of F₁(),F₂(), such that
A117: ( P₁[Aa,Bb] & the_rank_of F₅() = the_rank_of Aa ) and
A118: Aa * ((len f) + 1),(n + 1) <> 0. F₁() and
A119: for i, j being Nat st [i,j] in Indices Aa & i > len f & j <= n holds
Aa * i,j = 0. F₁() and
A120: for i, j being Nat st i in dom f holds
S₁[f,i,j,Aa] and
A121: for j being Nat st j in (dom Aa) \ {((len f) + 1)} & j <= F₂() holds
Aa * j,(n + 1) = 0. F₁() ;
take Aa ; :: thesis: ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[Aa,B'] & the_rank_of F₅() = 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. F₁() ) & f is one-to-one & len f <= n + 1 & len f <= F₂() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,Aa] ) ) )
take Bb ; :: thesis: ( P₁[Aa,Bb] & the_rank_of F₅() = 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. F₁() ) & f is one-to-one & len f <= n + 1 & len f <= F₂() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,Aa] ) ) )
thus ( P₁[Aa,Bb] & the_rank_of F₅() = 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. F₁() ) & f is one-to-one & len f <= n + 1 & len f <= F₂() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,Aa] ) )
take f' = f ^ <*(n + 1)*>; :: thesis: ( ( for i, j being Nat st [i,j] in Indices Aa & i > len f' & j <= n + 1 holds
Aa * i,j = 0. F₁() ) & f' is one-to-one & len f' <= n + 1 & len f' <= F₂() & rng f' c= Seg (n + 1) & ( for i, j being Nat st i in dom f' holds
S₁[f',i,j,Aa] ) )
A122: len f' = (len f) + 1 by FINSEQ_2:19;
A123: ( len Aa = F₂() & dom Aa = Seg (len Aa) ) by A4, FINSEQ_1:def 3, MATRIX_1:24;

A124: now

let i, j be Nat; :: thesis: ( [i,j] in Indices Aa & i > len f' & j <= n + 1 implies Aa * b₁,b₂ = 0. F₁() )
assume that
A125: [i,j] in Indices Aa and
A126: i > len f' and
A127: j <= n + 1 ; :: thesis: Aa * b₁,b₂ = 0. F₁()

per cases ( j <= n or j = n + 1 ) by A127, NAT_1:8;

suppose A128: j <= n ; :: thesis: Aa * b₁,b₂ = 0. F₁()

i > len f by A122, A126, NAT_1:13;
hence Aa * i,j = 0. F₁() by A119, A125, A128; :: thesis: verum

end;

suppose A129: j = n + 1 ; :: thesis: Aa * b₁,b₂ = 0. F₁()

i in dom Aa by A125, ZFMISC_1:106;
then ( i in (dom Aa) \ {((len f) + 1)} & i <= F₂() ) by A122, A123, A126, FINSEQ_1:3, ZFMISC_1:64;
hence Aa * i,j = 0. F₁() by A121, A129; :: thesis: verum

end;

end;

end;

A130: width Aa = F₃() by A4, MATRIX_1:24;
A131: len f' <= F₂() by A28, A29, A122, XXREAL_0:2;

A132: now

let i, j be Nat; :: thesis: ( i in dom f' implies ( Aa * i,(f' /. i) <> 0. F₁() & ( j in dom f' & i < j implies f' /. i < f' /. j ) & ( j in (dom f') \ {i} implies Aa * j,(f' /. i) = 0. F₁() ) & ( j in Seg (width Aa) & j < f' /. i implies Aa * i,j = 0. F₁() ) ) )
assume A133: i in dom f' ; :: thesis: ( Aa * i,(f' /. i) <> 0. F₁() & ( j in dom f' & i < j implies f' /. i < f' /. j ) & ( j in (dom f') \ {i} implies Aa * j,(f' /. i) = 0. F₁() ) & ( j in Seg (width Aa) & j < f' /. i implies Aa * i,j = 0. F₁() ) )
A134: dom f' = Seg ((len f) + 1) by A122, FINSEQ_1:def 3
.= (dom f) \/ {((len f) + 1)} by A31, FINSEQ_1:11 ;

A135: now

let k be Nat; :: thesis: ( k in dom f implies f /. k = f' /. k )
assume A136: k in dom f ; :: thesis: f /. k = f' /. k
A137: k in dom f' by A134, A136, XBOOLE_0:def 3;
thus f /. k = f . k by A136, PARTFUN1:def 8
.= f' . k by A136, FINSEQ_1:def 7
.= f' /. k by A137, PARTFUN1:def 8 ; :: thesis: verum

end;

now

per cases ( i in dom f or i in {((len f) + 1)} ) by A133, A134, XBOOLE_0:def 3;

suppose A138: i in dom f ; :: thesis: Aa * i,(f' /. i) <> 0. F₁()

then f /. i = f' /. i by A135;
hence Aa * i,(f' /. i) <> 0. F₁() by A120, A138; :: thesis: verum

end;

suppose A139: i in {((len f) + 1)} ; :: thesis: Aa * i,(f' /. i) <> 0. F₁()

A140: f' /. i = f' . i by A133, PARTFUN1:def 8;
i = (len f) + 1 by A139, TARSKI:def 1;
hence Aa * i,(f' /. i) <> 0. F₁() by A118, A140, FINSEQ_1:59; :: thesis: verum

end;

end;

end;

hence Aa * i,(f' /. i) <> 0. F₁() ; :: thesis: ( ( j in dom f' & i < j implies f' /. i < f' /. j ) & ( j in (dom f') \ {i} implies Aa * j,(f' /. i) = 0. F₁() ) & ( j in Seg (width Aa) & j < f' /. i implies Aa * i,j = 0. F₁() ) )
thus ( j in dom f' & i < j implies f' /. i < f' /. j ) :: thesis: ( ( j in (dom f') \ {i} implies Aa * j,(f' /. i) = 0. F₁() ) & ( j in Seg (width Aa) & j < f' /. i implies Aa * i,j = 0. F₁() ) )

proof

assume that
A141: j in dom f' and
A142: i < j ; :: thesis: f' /. i < f' /. 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 A133, A134, A141, XBOOLE_0:def 3;

suppose A143: ( j in {((len f) + 1)} & i in {((len f) + 1)} ) ; :: thesis: f' /. i < f' /. j

then i = (len f) + 1 by TARSKI:def 1;
hence f' /. i < f' /. j by A142, A143, TARSKI:def 1; :: thesis: verum

end;

suppose A144: ( j in {((len f) + 1)} & i in dom f ) ; :: thesis: f' /. i < f' /. j

then (len f) + 1 = j by TARSKI:def 1;
then A145: f' . j = n + 1 by FINSEQ_1:59;
( f /. i = f . i & f . i in rng f ) by A144, FUNCT_1:def 5, PARTFUN1:def 8;
then A146: f /. i <= n by A14, FINSEQ_1:3;
f' . j = f' /. j by A141, PARTFUN1:def 8;
then f /. i < f' /. j by A146, A145, NAT_1:13;
hence f' /. i < f' /. j by A135, A144; :: thesis: verum

end;

suppose ( j in dom f & i in {((len f) + 1)} ) ; :: thesis: f' /. i < f' /. j

then ( j <= len f & i = (len f) + 1 ) by A31, FINSEQ_1:3, TARSKI:def 1;
hence f' /. i < f' /. j by A142, NAT_1:13; :: thesis: verum

end;

suppose A147: ( j in dom f & i in dom f ) ; :: thesis: f' /. i < f' /. j

then ( f /. i = f' /. i & f /. j = f' /. j ) by A135;
hence f' /. i < f' /. j by A15, A142, A147; :: thesis: verum

end;

end;

end;

dom f' = Seg (len f') by FINSEQ_1:def 3;
then A148: dom f' c= dom Aa by A123, A131, FINSEQ_1:7;
thus ( j in (dom f') \ {i} implies Aa * j,(f' /. i) = 0. F₁() ) :: thesis: ( j in Seg (width Aa) & j < f' /. i implies Aa * i,j = 0. F₁() )

proof

assume A149: j in (dom f') \ {i} ; :: thesis: Aa * j,(f' /. i) = 0. F₁()

per cases ( i = (len f) + 1 or i <> (len f) + 1 ) ;

suppose A150: i = (len f) + 1 ; :: thesis: Aa * j,(f' /. i) = 0. F₁()

(len f) + 1 in {((len f) + 1)} by TARSKI:def 1;
then (len f) + 1 in dom f' by A134, XBOOLE_0:def 3;
then A151: f' . ((len f) + 1) = f' /. i by A150, PARTFUN1:def 8;
A152: j in dom f' by A149, ZFMISC_1:64;
j <> i by A149, ZFMISC_1:64;
then A153: j in (dom Aa) \ {i} by A148, A152, ZFMISC_1:64;
j <= F₂() by A123, A148, A152, FINSEQ_1:3;
then Aa * j,(n + 1) = 0. F₁() by A121, A150, A153;
hence Aa * j,(f' /. i) = 0. F₁() by A151, FINSEQ_1:59; :: thesis: verum

end;

suppose A154: i <> (len f) + 1 ; :: thesis: Aa * j,(f' /. i) = 0. F₁()

A155: j in dom f' by A149, XBOOLE_0:def 5;
A156: ( i in dom f or i in {((len f) + 1)} ) by A133, A134, XBOOLE_0:def 3;
then A157: f . i in rng f by A154, FUNCT_1:def 5, TARSKI:def 1;
A158: ( f /. i = f' /. i & f . i = f /. i ) by A135, A154, A156, PARTFUN1:def 8, TARSKI:def 1;
then A159: 1 <= f' /. i by A14, A157, FINSEQ_1:3;
A160: f' /. i <= n by A14, A158, A157, FINSEQ_1:3;
n <= F₃() by A7, NAT_1:13;
then f' /. i <= F₃() by A160, XXREAL_0:2;
then f' /. i in Seg (width Aa) by A130, A159;
then A161: [j,(f' /. i)] in Indices Aa by A148, A155, ZFMISC_1:106;

per cases ( j = (len f) + 1 or j <> (len f) + 1 ) ;

suppose j = (len f) + 1 ; :: thesis: Aa * j,(f' /. i) = 0. F₁()

then j > len f by NAT_1:13;
hence Aa * j,(f' /. i) = 0. F₁() by A119, A160, A161; :: thesis: verum

end;

suppose A162: j <> (len f) + 1 ; :: thesis: Aa * j,(f' /. i) = 0. F₁()

j in dom f' by A149, XBOOLE_0:def 5;
then A163: ( j in dom f or j in {((len f) + 1)} ) by A134, XBOOLE_0:def 3;
j <> i by A149, ZFMISC_1:64;
then j in (dom f) \ {i} by A162, A163, TARSKI:def 1, ZFMISC_1:64;
then Aa * j,(f /. i) = 0. F₁() by A120, A154, A156, TARSKI:def 1;
hence Aa * j,(f' /. i) = 0. F₁() by A135, A154, A156, TARSKI:def 1; :: thesis: verum

end;

end;

end;

end;

end;

thus ( j in Seg (width Aa) & j < f' /. i implies Aa * i,j = 0. F₁() ) :: thesis: verum

proof

assume that
A164: j in Seg (width Aa) and
A165: j < f' /. i ; :: thesis: Aa * i,j = 0. F₁()

per cases ( i in dom f or not i in dom f ) ;

suppose A166: i in dom f ; :: thesis: Aa * i,j = 0. F₁()

then f' /. i = f /. i by A135;
hence Aa * i,j = 0. F₁() by A120, A164, A165, A166; :: thesis: verum

end;

suppose A167: not i in dom f ; :: thesis: Aa * i,j = 0. F₁()

( i in dom f or i in {((len f) + 1)} ) by A133, A134, XBOOLE_0:def 3;
then A168: i = (len f) + 1 by A167, TARSKI:def 1;
then A169: f' . i = n + 1 by FINSEQ_1:59;
f' . i = f' /. i by A133, PARTFUN1:def 8;
then A170: j <= n by A165, A169, NAT_1:13;
A171: i > len f by A168, NAT_1:13;
[i,j] in Indices Aa by A133, A148, A164, ZFMISC_1:106;
hence Aa * i,j = 0. F₁() by A119, A170, A171; :: thesis: verum

end;

end;

end;

end;

A172: ( rng <*(n + 1)*> = {(n + 1)} & (rng f) \/ {(n + 1)} c= (Seg n) \/ {(n + 1)} ) by A14, FINSEQ_1:55, XBOOLE_1:9;
A173: (Seg n) \/ {(n + 1)} = Seg (n + 1) by FINSEQ_1:11;
( rng f misses {(n + 1)} & <*(n + 1)*> is one-to-one ) by A14, FINSEQ_3:15, FINSEQ_3:102, XBOOLE_1:63;
hence ( ( for i, j being Nat st [i,j] in Indices Aa & i > len f' & j <= n + 1 holds
Aa * i,j = 0. F₁() ) & f' is one-to-one & len f' <= n + 1 & len f' <= F₂() & rng f' c= Seg (n + 1) & ( for i, j being Nat st i in dom f' holds
S₁[f',i,j,Aa] ) ) by A11, A12, A28, A29, A122, A124, A172, A173, A132, FINSEQ_1:44, FINSEQ_3:98, XREAL_1:8, XXREAL_0:2; :: thesis: verum

end;

end;

end;

A174: S₂[ 0 ]

proof

assume 0 <= F₃() ; :: thesis: ex A' being Matrix of the carrier of F₁(),F₂(), ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= 0 holds
A' * i,j = 0. F₁() ) & f is one-to-one & len f <= 0 & len f <= F₂() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) ) )
take A' = F₅(); :: thesis: ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= 0 holds
A' * i,j = 0. F₁() ) & f is one-to-one & len f <= 0 & len f <= F₂() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) ) )
take B' = F₆(); :: thesis: ( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= 0 holds
A' * i,j = 0. F₁() ) & f is one-to-one & len f <= 0 & len f <= F₂() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) ) )
thus ( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' ) by A1; :: thesis: ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= 0 holds
A' * i,j = 0. F₁() ) & f is one-to-one & len f <= 0 & len f <= F₂() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) )
take f = <*> NAT ; :: thesis: ( ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= 0 holds
A' * i,j = 0. F₁() ) & f is one-to-one & len f <= 0 & len f <= F₂() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) )

now

let i, j be Nat; :: thesis: ( [i,j] in Indices A' & i > len f & j <= 0 implies A' * i,j = 0. F₁() )
assume that
A175: [i,j] in Indices A' and
i > len f and
A176: j <= 0 ; :: thesis: A' * i,j = 0. F₁()
j in Seg (width A') by A175, ZFMISC_1:106;
hence A' * i,j = 0. F₁() by A176; :: thesis: verum

end;

hence ( ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= 0 holds
A' * i,j = 0. F₁() ) & f is one-to-one & len f <= 0 & len f <= F₂() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) ) ; :: thesis: verum

end;

for n being Nat holds S₂[n] from NAT_1:sch 2(A174, A5);
then consider A' being Matrix of the carrier of F₁(),F₂(),, B' being Matrix of the carrier of F₁(),F₂(), such that
A177: P₁[A',B'] and
A178: the_rank_of F₅() = the_rank_of A' and
A179: ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= F₃() holds
A' * i,j = 0. F₁() ) & f is one-to-one & len f <= F₃() & len f <= F₂() & rng f c= Seg F₃() & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) ) ;
consider f being FinSequence of NAT such that
A180: for i, j being Nat st [i,j] in Indices A' & i > len f & j <= F₃() holds
A' * i,j = 0. F₁() and
A181: f is one-to-one and
len f <= F₃() and
A182: len f <= F₂() and
A183: rng f c= Seg F₃() and
A184: for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] by A179;
A185: len A' = F₂() by A4, MATRIX_1:24;
take A' ; :: thesis: ex B' being Matrix of the carrier of F₁(),F₂(), st
( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & ( for i being Nat st i in dom A' & i > the_rank_of F₅() holds
Line A',i = F₃() |-> (0. F₁()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) ) )
take B' ; :: thesis: ( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' & ( for i being Nat st i in dom A' & i > the_rank_of F₅() holds
Line A',i = F₃() |-> (0. F₁()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) ) )
thus ( P₁[A',B'] & the_rank_of F₅() = the_rank_of A' ) by A177, A178; :: thesis: ( ( for i being Nat st i in dom A' & i > the_rank_of F₅() holds
Line A',i = F₃() |-> (0. F₁()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) ) )
A186: dom A' = Seg (len A') by FINSEQ_1:def 3;
set L = len f;
A187: Seg (len f) c= Seg F₂() by A182, FINSEQ_1:7;
( idseq (len f) is FinSequence of NAT & len (idseq (len f)) = len f ) by FINSEQ_1:def 18, FINSEQ_2:52;
then reconsider idL = idseq (len f), F' = f as Element of (len f) -tuples_on NAT by FINSEQ_2:110;
set S = Segm A',idL,F';
A188: dom f = Seg (len f) by FINSEQ_1:def 3;
set D = diagonal_of_Matrix (Segm A',idL,F');
A189: Indices (Segm A',idL,F') = [:(Seg (len f)),(Seg (len f)):] by MATRIX_1:25;
for k being Element of NAT st k in dom (diagonal_of_Matrix (Segm A',idL,F')) holds
(diagonal_of_Matrix (Segm A',idL,F')) . k <> 0. F₁()

proof

A190: len (diagonal_of_Matrix (Segm A',idL,F')) = len f by MATRIX_3:def 10;
let k be Element of NAT ; :: thesis: ( k in dom (diagonal_of_Matrix (Segm A',idL,F')) implies (diagonal_of_Matrix (Segm A',idL,F')) . k <> 0. F₁() )
assume k in dom (diagonal_of_Matrix (Segm A',idL,F')) ; :: thesis: (diagonal_of_Matrix (Segm A',idL,F')) . k <> 0. F₁()
then A191: k in Seg (len f) by A190, FINSEQ_1:def 3;
then [k,k] in Indices (Segm A',idL,F') by A189, ZFMISC_1:106;
then (Segm A',idL,F') * k,k = A' * (idL . k),(f . k) by MATRIX13:def 1
.= A' * k,(f . k) by A191, FINSEQ_2:57
.= A' * k,(f /. k) by A188, A191, PARTFUN1:def 8 ;
then (Segm A',idL,F') * k,k <> 0. F₁() by A184, A188, A191;
hence (diagonal_of_Matrix (Segm A',idL,F')) . k <> 0. F₁() by A191, MATRIX_3:def 10; :: thesis: verum

end;

then A192: Product (diagonal_of_Matrix (Segm A',idL,F')) <> 0. F₁() by FVSUM_1:107;

now

let i, j be Nat; :: thesis: ( [i,j] in Indices (Segm A',idL,F') & i > j implies (Segm A',idL,F') * i,j = 0. F₁() )
assume A193: [i,j] in Indices (Segm A',idL,F') ; :: thesis: ( i > j implies (Segm A',idL,F') * i,j = 0. F₁() )
A194: i in Seg (len f) by A189, A193, ZFMISC_1:106;
assume i > j ; :: thesis: (Segm A',idL,F') * i,j = 0. F₁()
then A195: i in (dom f) \ {j} by A188, A194, ZFMISC_1:64;
reconsider i' = i, j' = j as Element of NAT by ORDINAL1:def 13;
A196: j in Seg (len f) by A189, A193, ZFMISC_1:106;
thus (Segm A',idL,F') * i,j = A' * (idL . i'),(f . j') by A193, MATRIX13:def 1
.= A' * i,(f . j) by A194, FINSEQ_2:57
.= A' * i,(f /. j) by A188, A196, PARTFUN1:def 8
.= 0. F₁() by A184, A188, A196, A195 ; :: thesis: verum

end;

then Segm A',idL,F' is Upper_Triangular_Matrix of len f,F₁() by MATRIX_2:def 3;
then A197: Det (Segm A',idL,F') <> 0. F₁() by A192, MATRIX13:7;
A198: len (Segm A',(Seg (len f)),(Seg (width A'))) = card (Seg (len f)) by MATRIX_1:def 3;
A199: width A' = F₃() by A4, MATRIX_1:24;
rng idL = Seg (len f) by RELAT_1:71;
then [:(rng idL),(rng F'):] c= Indices A' by A183, A187, A185, A186, A199, ZFMISC_1:119;
then A200: the_rank_of A' >= len f by A197, MATRIX13:76;

A201: now

set w0 = (width A') |-> (0. F₁());
let i be Nat; :: thesis: ( i in (dom A') \ (Seg (len f)) implies Line A',i = (width A') |-> (0. F₁()) )
assume A202: i in (dom A') \ (Seg (len f)) ; :: thesis: Line A',i = (width A') |-> (0. F₁())
set LA = Line A',i;

A203: now

not i in Seg (len f) by A202, XBOOLE_0:def 5;
then A204: ( i > len f or i < 1 ) by A202;
let j be Nat; :: thesis: ( 1 <= j & j <= width A' implies (Line A',i) . j = ((width A') |-> (0. F₁())) . j )
assume that
A205: 1 <= j and
A206: j <= width A' ; :: thesis: (Line A',i) . j = ((width A') |-> (0. F₁())) . j
j in NAT by ORDINAL1:def 13;
then A207: j in Seg (width A') by A205, A206;
A208: i in dom A' by A202, XBOOLE_0:def 5;
then A209: [i,j] in Indices A' by A207, ZFMISC_1:106;
thus (Line A',i) . j = A' * i,j by A207, MATRIX_1:def 8
.= 0. F₁() by A180, A186, A199, A206, A208, A209, A204, FINSEQ_1:3
.= ((width A') |-> (0. F₁())) . j by A207, FINSEQ_2:71 ; :: thesis: verum

end;

( len (Line A',i) = width A' & len ((width A') |-> (0. F₁())) = width A' ) by FINSEQ_1:def 18;
hence Line A',i = (width A') |-> (0. F₁()) by A203, FINSEQ_1:18; :: thesis: verum

end;

then the_rank_of A' = the_rank_of (Segm A',(Seg (len f)),(Seg (width A'))) by A187, A185, A186, Th11;
then the_rank_of A' <= card (Seg (len f)) by A198, MATRIX13:74;
then A210: the_rank_of A' <= len f by FINSEQ_1:78;
then A211: the_rank_of F₅() = len f by A178, A200, XXREAL_0:1;
thus for i being Nat st i in dom A' & i > the_rank_of F₅() holds
Line A',i = F₃() |-> (0. F₁()) :: thesis: ex f being FinSequence of NAT st
( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) )

proof

let i be Nat; :: thesis: ( i in dom A' & i > the_rank_of F₅() implies Line A',i = F₃() |-> (0. F₁()) )
assume that
A212: i in dom A' and
A213: i > the_rank_of F₅() ; :: thesis: Line A',i = F₃() |-> (0. F₁())
not i in Seg (len f) by A211, A213, FINSEQ_1:3;
then i in (dom A') \ (Seg (len f)) by A212, XBOOLE_0:def 5;
hence Line A',i = F₃() |-> (0. F₁()) by A199, A201; :: thesis: verum

end;

take f ; :: thesis: ( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) )
thus ( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) ) by A4, A181, A183, A184, A200, A210, MATRIX_1:24, XXREAL_0:1; :: thesis: verum

end;

end;

end;

then consider A' being Matrix of the carrier of F₁(),F₂(),, B' being Matrix of the carrier of F₁(),F₂(), such that
A214: P₁[A',B'] and
A215: the_rank_of F₅() = the_rank_of A' and
A216: for i being Nat st i in dom A' & i > the_rank_of F₅() holds
Line A',i = F₃() |-> (0. F₁()) and
A217: ex f being FinSequence of NAT st
( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] ) ) ;
consider f being FinSequence of NAT such that
A218: len f = the_rank_of A' and
A219: f is one-to-one and
A220: rng f c= Seg (width A') and
A221: for i, j being Nat st i in dom f holds
S₁[f,i,j,A'] by A217;
not 0 in rng f by A220;
then reconsider rngf = rng f as finite without_zero Subset of by A220, PSCOMP_1:def 1, XBOOLE_1:1;
A222: ( F₂() = 0 or F₂() > 0 ) ;
set S = Segm A',(Seg (card rngf)),rngf;
A223: dom f = Seg (the_rank_of F₅()) by A215, A218, FINSEQ_1:def 3;
take A' ; :: thesis: ex B' being Matrix of the carrier of F₁(),F₂(), ex N being finite without_zero Subset of st
( N c= Seg F₃() & the_rank_of F₅() = the_rank_of A' & the_rank_of F₅() = card N & P₁[A',B'] & Segm A',(Seg (card N)),N is diagonal & ( for i being Nat st i in Seg (card N) holds
A' * i,((Sgm N) /. i) <> 0. F₁() ) & ( for i being Nat st i in dom A' & i > card N holds
Line A',i = F₃() |-> (0. F₁()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width A') & j < (Sgm N) . i holds
A' * i,j = 0. F₁() ) )
take B' ; :: thesis: ex N being finite without_zero Subset of st
( N c= Seg F₃() & the_rank_of F₅() = the_rank_of A' & the_rank_of F₅() = card N & P₁[A',B'] & Segm A',(Seg (card N)),N is diagonal & ( for i being Nat st i in Seg (card N) holds
A' * i,((Sgm N) /. i) <> 0. F₁() ) & ( for i being Nat st i in dom A' & i > card N holds
Line A',i = F₃() |-> (0. F₁()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width A') & j < (Sgm N) . i holds
A' * i,j = 0. F₁() ) )
take rngf ; :: thesis: ( rngf c= Seg F₃() & the_rank_of F₅() = the_rank_of A' & the_rank_of F₅() = card rngf & P₁[A',B'] & Segm A',(Seg (card rngf)),rngf is diagonal & ( for i being Nat st i in Seg (card rngf) holds
A' * i,((Sgm rngf) /. i) <> 0. F₁() ) & ( for i being Nat st i in dom A' & i > card rngf holds
Line A',i = F₃() |-> (0. F₁()) ) & ( for i, j being Nat st i in Seg (card rngf) & j in Seg (width A') & j < (Sgm rngf) . i holds
A' * i,j = 0. F₁() ) )
len A' = F₂() by MATRIX_1:def 3;
then ( width A' = 0 or width A' = F₃() ) by A222, MATRIX_1:24, MATRIX_1:def 4;
then Seg (width A') c= Seg F₃() by FINSEQ_1:7;
hence ( rngf c= Seg F₃() & the_rank_of F₅() = the_rank_of A' ) by A215, A220, XBOOLE_1:1; :: thesis: ( the_rank_of F₅() = card rngf & P₁[A',B'] & Segm A',(Seg (card rngf)),rngf is diagonal & ( for i being Nat st i in Seg (card rngf) holds
A' * i,((Sgm rngf) /. i) <> 0. F₁() ) & ( for i being Nat st i in dom A' & i > card rngf holds
Line A',i = F₃() |-> (0. F₁()) ) & ( for i, j being Nat st i in Seg (card rngf) & j in Seg (width A') & j < (Sgm rngf) . i holds
A' * i,j = 0. F₁() ) )
dom f,rngf are_equipotent by A219, WELLORD2:def 4;
hence A224: card rngf = card (dom f) by CARD_1:21
.= card (Seg (the_rank_of F₅())) by A215, A218, FINSEQ_1:def 3
.= the_rank_of F₅() by FINSEQ_1:78 ;
:: thesis: ( P₁[A',B'] & Segm A',(Seg (card rngf)),rngf is diagonal & ( for i being Nat st i in Seg (card rngf) holds
A' * i,((Sgm rngf) /. i) <> 0. F₁() ) & ( for i being Nat st i in dom A' & i > card rngf holds
Line A',i = F₃() |-> (0. F₁()) ) & ( for i, j being Nat st i in Seg (card rngf) & j in Seg (width A') & j < (Sgm rngf) . i holds
A' * i,j = 0. F₁() ) )

now

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 A225, PARTFUN1:def 8;
hence f . i < f . j by A221, A225, A226; :: thesis: verum

end;

then A227: Sgm rngf = f by A219, A220, Th6;
thus P₁[A',B'] by A214; :: thesis: ( Segm A',(Seg (card rngf)),rngf is diagonal & ( for i being Nat st i in Seg (card rngf) holds
A' * i,((Sgm rngf) /. i) <> 0. F₁() ) & ( for i being Nat st i in dom A' & i > card rngf holds
Line A',i = F₃() |-> (0. F₁()) ) & ( for i, j being Nat st i in Seg (card rngf) & j in Seg (width A') & j < (Sgm rngf) . i holds
A' * i,j = 0. F₁() ) )
A228: card (Seg (card rngf)) = card rngf by FINSEQ_1:78;
then A229: Indices (Segm A',(Seg (card rngf)),rngf) = [:(Seg (the_rank_of F₅())),(Seg (the_rank_of F₅())):] by A224, MATRIX_1:25;

now

let i, j be Element of NAT ; :: thesis: ( i in Seg (the_rank_of F₅()) & j in Seg (the_rank_of F₅()) & i <> j implies (Segm A',(Seg (card rngf)),rngf) * i,j = 0. F₁() )
assume that
A230: i in Seg (the_rank_of F₅()) and
A231: j in Seg (the_rank_of F₅()) and
A232: i <> j ; :: thesis: (Segm A',(Seg (card rngf)),rngf) * i,j = 0. F₁()
A233: i in (dom f) \ {j} by A223, A230, A232, ZFMISC_1:64;
A234: (idseq (the_rank_of F₅())) . i = i by A230, FINSEQ_2:57;
[i,j] in Indices (Segm A',(Seg (card rngf)),rngf) by A229, A230, A231, ZFMISC_1:106;
then (Segm A',(Seg (card rngf)),rngf) * i,j = A' * ((Sgm (Seg (the_rank_of F₅()))) . i),(f . j) by A224, A227, MATRIX13:def 1
.= A' * i,(f . j) by A234, FINSEQ_3:54
.= A' * i,(f /. j) by A223, A231, PARTFUN1:def 8 ;
hence (Segm A',(Seg (card rngf)),rngf) * i,j = 0. F₁() by A221, A223, A231, A233; :: thesis: verum

end;

hence Segm A',(Seg (card rngf)),rngf is diagonal by A224, A228, MATRIX_7:def 2; :: thesis: ( ( for i being Nat st i in Seg (card rngf) holds
A' * i,((Sgm rngf) /. i) <> 0. F₁() ) & ( for i being Nat st i in dom A' & i > card rngf holds
Line A',i = F₃() |-> (0. F₁()) ) & ( for i, j being Nat st i in Seg (card rngf) & j in Seg (width A') & j < (Sgm rngf) . i holds
A' * i,j = 0. F₁() ) )
thus for i being Nat st i in Seg (card rngf) holds
A' * i,((Sgm rngf) /. i) <> 0. F₁() by A221, A224, A227, A223; :: thesis: ( ( for i being Nat st i in dom A' & i > card rngf holds
Line A',i = F₃() |-> (0. F₁()) ) & ( for i, j being Nat st i in Seg (card rngf) & j in Seg (width A') & j < (Sgm rngf) . i holds
A' * i,j = 0. F₁() ) )
thus for i being Nat st i in dom A' & i > card rngf holds
Line A',i = F₃() |-> (0. F₁()) by A216, A224; :: thesis: for i, j being Nat st i in Seg (card rngf) & j in Seg (width A') & j < (Sgm rngf) . i holds
A' * i,j = 0. F₁()
let i, j be Nat; :: thesis: ( i in Seg (card rngf) & j in Seg (width A') & j < (Sgm rngf) . i implies A' * i,j = 0. F₁() )
assume that
A235: i in Seg (card rngf) and
A236: j in Seg (width A') and
A237: j < (Sgm rngf) . i ; :: thesis: A' * i,j = 0. F₁()
j < f /. i by A224, A227, A223, A235, A237, PARTFUN1:def 8;
hence A' * i,j = 0. F₁() by A221, A224, A223, A235, A236; :: thesis: verum