defpred S_{1}[ FinSequence of NAT , Nat, Nat, Matrix of F_{2}(),F_{3}(),F_{1}()] means ( $4 * ($2,($1 /. $2)) <> 0. F_{1}() & ( $3 in dom $1 & $2 < $3 implies $1 /. $2 < $1 /. $3 ) & ( $3 in (dom $1) \ {$2} implies $4 * ($3,($1 /. $2)) = 0. F_{1}() ) & ( $3 in Seg (width $4) & $3 < $1 /. $2 implies $4 * ($2,$3) = 0. F_{1}() ) );

set r = the_rank_of F_{5}();

ex A9 being Matrix of F_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = the_rank_of A9 & ( for i being Nat st i in dom A9 & i > the_rank_of F_{5}() holds

Line (A9,i) = F_{3}() |-> (0. F_{1}()) ) & 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

S_{1}[f,i,j,A9] ) ) )
_{2}(),F_{3}(),F_{1}(), B9 being Matrix of F_{2}(),F_{4}(),F_{1}() such that

A214: P_{1}[A9,B9]
and

A215: the_rank_of F_{5}() = the_rank_of A9
and

A216: for i being Nat st i in dom A9 & i > the_rank_of F_{5}() holds

Line (A9,i) = F_{3}() |-> (0. F_{1}())
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

S_{1}[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

S_{1}[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 A220, MEASURE6:def 2, XBOOLE_1:1;

A222: ( F_{2}() = 0 or F_{2}() > 0 )
;

set S = Segm (A9,(Seg (card rngf)),rngf);

A223: dom f = Seg (the_rank_of F_{5}())
by A215, A218, FINSEQ_1:def 3;

take A9 ; :: thesis: ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() ex N being finite without_zero Subset of NAT st

( N c= Seg F_{3}() & the_rank_of F_{5}() = the_rank_of A9 & the_rank_of F_{5}() = card N & P_{1}[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. F_{1}() ) & ( for i being Nat st i in dom A9 & i > card N holds

Line (A9,i) = F_{3}() |-> (0. F_{1}()) ) & ( 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. F_{1}() ) )

take B9 ; :: thesis: ex N being finite without_zero Subset of NAT st

( N c= Seg F_{3}() & the_rank_of F_{5}() = the_rank_of A9 & the_rank_of F_{5}() = card N & P_{1}[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. F_{1}() ) & ( for i being Nat st i in dom A9 & i > card N holds

Line (A9,i) = F_{3}() |-> (0. F_{1}()) ) & ( 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. F_{1}() ) )

take rngf ; :: thesis: ( rngf c= Seg F_{3}() & the_rank_of F_{5}() = the_rank_of A9 & the_rank_of F_{5}() = card rngf & P_{1}[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. F_{1}() ) & ( for i being Nat st i in dom A9 & i > card rngf holds

Line (A9,i) = F_{3}() |-> (0. F_{1}()) ) & ( 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. F_{1}() ) )

len A9 = F_{2}()
by MATRIX_0:def 2;

then ( width A9 = 0 or width A9 = F_{3}() )
by A222, MATRIX_0:23, MATRIX_0:def 3;

then Seg (width A9) c= Seg F_{3}()
;

hence ( rngf c= Seg F_{3}() & the_rank_of F_{5}() = the_rank_of A9 )
by A215, A220; :: thesis: ( the_rank_of F_{5}() = card rngf & P_{1}[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. F_{1}() ) & ( for i being Nat st i in dom A9 & i > card rngf holds

Line (A9,i) = F_{3}() |-> (0. F_{1}()) ) & ( 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. F_{1}() ) )

dom f,rngf are_equipotent by A219, WELLORD2:def 4;

hence A224: card rngf = card (dom f) by CARD_1:5

.= card (Seg (the_rank_of F_{5}()))
by A215, A218, FINSEQ_1:def 3

.= the_rank_of F_{5}()
by FINSEQ_1:57
;

:: thesis: ( P_{1}[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. F_{1}() ) & ( for i being Nat st i in dom A9 & i > card rngf holds

Line (A9,i) = F_{3}() |-> (0. F_{1}()) ) & ( 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. F_{1}() ) )

thus P_{1}[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. F_{1}() ) & ( for i being Nat st i in dom A9 & i > card rngf holds

Line (A9,i) = F_{3}() |-> (0. F_{1}()) ) & ( 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. F_{1}() ) )

A228: card (Seg (card rngf)) = card rngf by FINSEQ_1:57;

then A229: Indices (Segm (A9,(Seg (card rngf)),rngf)) = [:(Seg (the_rank_of F_{5}())),(Seg (the_rank_of F_{5}())):]
by A224, MATRIX_0:24;

A9 * (i,((Sgm rngf) /. i)) <> 0. F_{1}() ) & ( for i being Nat st i in dom A9 & i > card rngf holds

Line (A9,i) = F_{3}() |-> (0. F_{1}()) ) & ( 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. F_{1}() ) )

thus for i being Nat st i in Seg (card rngf) holds

A9 * (i,((Sgm rngf) /. i)) <> 0. F_{1}()
by A221, A224, A227, A223; :: thesis: ( ( for i being Nat st i in dom A9 & i > card rngf holds

Line (A9,i) = F_{3}() |-> (0. F_{1}()) ) & ( 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. F_{1}() ) )

thus for i being Nat st i in dom A9 & i > card rngf holds

Line (A9,i) = F_{3}() |-> (0. F_{1}())
by A216, A224; :: 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. F_{1}()

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. F_{1}() )

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. F_{1}()

j < f /. i by A224, A227, A223, A235, A237, PARTFUN1:def 6;

hence A9 * (i,j) = 0. F_{1}()
by A221, A224, A223, A235, A236; :: thesis: verum

set r = the_rank_of F

ex A9 being Matrix of F

( P

Line (A9,i) = F

( 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

S

proof
end;

then consider A9 being Matrix of Fper cases
( F_{2}() = 0 or F_{2}() > 0 )
;

end;

suppose A3:
F_{2}() = 0
; :: thesis: ex A9 being Matrix of F_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = the_rank_of A9 & ( for i being Nat st i in dom A9 & i > the_rank_of F_{5}() holds

Line (A9,i) = F_{3}() |-> (0. F_{1}()) ) & 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

S_{1}[f,i,j,A9] ) ) )

( P

Line (A9,i) = F

( 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

S

take A9 = F_{5}(); :: thesis: ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = the_rank_of A9 & ( for i being Nat st i in dom A9 & i > the_rank_of F_{5}() holds

Line (A9,i) = F_{3}() |-> (0. F_{1}()) ) & 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

S_{1}[f,i,j,A9] ) ) )

take B9 = F_{6}(); :: thesis: ( P_{1}[A9,B9] & the_rank_of F_{5}() = the_rank_of A9 & ( for i being Nat st i in dom A9 & i > the_rank_of F_{5}() holds

Line (A9,i) = F_{3}() |-> (0. F_{1}()) ) & 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

S_{1}[f,i,j,A9] ) ) )

( dom A9 = Seg (len A9) & len A9 = 0 ) by A3, FINSEQ_1:def 3, MATRIX_0:def 2;

hence ( P_{1}[A9,B9] & the_rank_of F_{5}() = the_rank_of A9 & ( for i being Nat st i in dom A9 & i > the_rank_of F_{5}() holds

Line (A9,i) = F_{3}() |-> (0. F_{1}()) ) )
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

S_{1}[f,i,j,A9] ) )

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

S_{1}[ <*> NAT,i,j,A9] ) )

len A9 = 0 by A3, MATRIX_0:22;

hence ( len (<*> NAT) = the_rank_of A9 & <*> NAT is one-to-one & rng (<*> NAT) c= Seg (width A9) & ( for i, j being Nat st i in dom (<*> NAT) holds

S_{1}[ <*> NAT,i,j,A9] ) )
by MATRIX13:74; :: thesis: verum

end;( P

Line (A9,i) = F

( 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

S

take B9 = F

Line (A9,i) = F

( 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

S

( dom A9 = Seg (len A9) & len A9 = 0 ) by A3, FINSEQ_1:def 3, MATRIX_0:def 2;

hence ( P

Line (A9,i) = F

( 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

S

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

S

len A9 = 0 by A3, MATRIX_0:22;

hence ( len (<*> NAT) = the_rank_of A9 & <*> NAT is one-to-one & rng (<*> NAT) c= Seg (width A9) & ( for i, j being Nat st i in dom (<*> NAT) holds

S

suppose A4:
F_{2}() > 0
; :: thesis: ex A9 being Matrix of F_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = the_rank_of A9 & ( for i being Nat st i in dom A9 & i > the_rank_of F_{5}() holds

Line (A9,i) = F_{3}() |-> (0. F_{1}()) ) & 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

S_{1}[f,i,j,A9] ) ) )

( P

Line (A9,i) = F

( 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

S

defpred S_{2}[ Nat] means ( $1 <= F_{3}() implies ex A9 being Matrix of F_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = 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. F_{1}() ) & f is one-to-one & len f <= $1 & len f <= F_{2}() & rng f c= Seg $1 & ( for i, j being Nat st i in dom f holds

S_{1}[f,i,j,A9] ) ) ) );

A5: for n being Nat st S_{2}[n] holds

S_{2}[n + 1]
_{2}[ 0 ]
_{2}[n]
from NAT_1:sch 2(A174, A5);

then consider A9 being Matrix of F_{2}(),F_{3}(),F_{1}(), B9 being Matrix of F_{2}(),F_{4}(),F_{1}() such that

A177: P_{1}[A9,B9]
and

A178: the_rank_of F_{5}() = 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 <= F_{3}() holds

A9 * (i,j) = 0. F_{1}() ) & f is one-to-one & len f <= F_{3}() & len f <= F_{2}() & rng f c= Seg F_{3}() & ( for i, j being Nat st i in dom f holds

S_{1}[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 <= F_{3}() holds

A9 * (i,j) = 0. F_{1}()
and

A181: f is one-to-one and

len f <= F_{3}()
and

A182: len f <= F_{2}()
and

A183: rng f c= Seg F_{3}()
and

A184: for i, j being Nat st i in dom f holds

S_{1}[f,i,j,A9]
by A179;

A185: len A9 = F_{2}()
by A4, MATRIX_0:23;

take A9 ; :: thesis: ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = the_rank_of A9 & ( for i being Nat st i in dom A9 & i > the_rank_of F_{5}() holds

Line (A9,i) = F_{3}() |-> (0. F_{1}()) ) & 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

S_{1}[f,i,j,A9] ) ) )

take B9 ; :: thesis: ( P_{1}[A9,B9] & the_rank_of F_{5}() = the_rank_of A9 & ( for i being Nat st i in dom A9 & i > the_rank_of F_{5}() holds

Line (A9,i) = F_{3}() |-> (0. F_{1}()) ) & 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

S_{1}[f,i,j,A9] ) ) )

thus ( P_{1}[A9,B9] & the_rank_of F_{5}() = the_rank_of A9 )
by A177, A178; :: thesis: ( ( for i being Nat st i in dom A9 & i > the_rank_of F_{5}() holds

Line (A9,i) = F_{3}() |-> (0. F_{1}()) ) & 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

S_{1}[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 F_{2}()
by A182, FINSEQ_1:5;

( idseq (len f) is FinSequence of NAT & len (idseq (len f)) = len f ) by CARD_1:def 7, FINSEQ_2:48;

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. F_{1}()
_{1}()
by FVSUM_1:82;

_{1}()
by MATRIX_1:def 8;

then A197: Det (Segm (A9,idL,F9)) <> 0. F_{1}()
by A192, MATRIX13:7;

A198: len (Segm (A9,(Seg (len f)),(Seg (width A9)))) = card (Seg (len f)) by MATRIX_0:def 2;

A199: width A9 = F_{3}()
by A4, MATRIX_0:23;

[:(rng idL),(rng F9):] c= Indices A9 by A183, A187, A185, A186, A199, ZFMISC_1:96;

then A200: the_rank_of A9 >= len f by A197, MATRIX13:76;

then the_rank_of A9 <= card (Seg (len f)) by A198, MATRIX13:74;

then A210: the_rank_of A9 <= len f by FINSEQ_1:57;

then A211: the_rank_of F_{5}() = len f
by A178, A200, XXREAL_0:1;

thus for i being Nat st i in dom A9 & i > the_rank_of F_{5}() holds

Line (A9,i) = F_{3}() |-> (0. F_{1}())
:: 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

S_{1}[f,i,j,A9] ) )

S_{1}[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

S_{1}[f,i,j,A9] ) )
by A4, A181, A183, A184, A200, A210, MATRIX_0:23, XXREAL_0:1; :: thesis: verum

end;( P

( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= $1 holds

A9 * (i,j) = 0. F

S

A5: for n being Nat st S

S

proof

A174:
S
let n be Nat; :: thesis: ( S_{2}[n] implies S_{2}[n + 1] )

assume A6: S_{2}[n]
; :: thesis: S_{2}[n + 1]

set n1 = n + 1;

assume A7: n + 1 <= F_{3}()
; :: thesis: ex A9 being Matrix of F_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = 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. F_{1}() ) & f is one-to-one & len f <= n + 1 & len f <= F_{2}() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds

S_{1}[f,i,j,A9] ) ) )

then consider A9 being Matrix of F_{2}(),F_{3}(),F_{1}(), B9 being Matrix of F_{2}(),F_{4}(),F_{1}() such that

A8: ( P_{1}[A9,B9] & the_rank_of F_{5}() = 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. F_{1}() ) & f is one-to-one & len f <= n & len f <= F_{2}() & rng f c= Seg n & ( for i, j being Nat st i in dom f holds

S_{1}[f,i,j,A9] ) )
by A6, NAT_1:13;

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. F_{1}()
and

A11: f is one-to-one and

A12: len f <= n and

A13: len f <= F_{2}()
and

A14: rng f c= Seg n and

A15: for i, j being Nat st i in dom f holds

S_{1}[f,i,j,A9]
by A9;

end;assume A6: S

set n1 = n + 1;

assume A7: n + 1 <= F

( P

( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n + 1 holds

A9 * (i,j) = 0. F

S

then consider A9 being Matrix of F

A8: ( P

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. F

S

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. F

A11: f is one-to-one and

A12: len f <= n and

A13: len f <= F

A14: rng f c= Seg n and

A15: for i, j being Nat st i in dom f holds

S

per cases
( for i, j being Nat st [i,j] in Indices A9 & i > len f & j = n + 1 holds

A9 * (i,j) = 0. F_{1}() or ex i, j being Nat st

( [i,j] in Indices A9 & i > len f & j = n + 1 & A9 * (i,j) <> 0. F_{1}() ) )
;

end;

A9 * (i,j) = 0. F

( [i,j] in Indices A9 & i > len f & j = n + 1 & A9 * (i,j) <> 0. F

suppose A16:
for i, j being Nat st [i,j] in Indices A9 & i > len f & j = n + 1 holds

A9 * (i,j) = 0. F_{1}()
; :: thesis: ex A9 being Matrix of F_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = 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. F_{1}() ) & f is one-to-one & len f <= n + 1 & len f <= F_{2}() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds

S_{1}[f,i,j,A9] ) ) )

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 A12, NAT_1:12;

hence ex A9 being Matrix of F_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = 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. F_{1}() ) & f is one-to-one & len f <= n + 1 & len f <= F_{2}() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds

S_{1}[f,i,j,A9] ) ) )
by A8, A11, A13, A15, A17, A20; :: thesis: verum

end;

A9 * (i,j) = 0. F

( P

( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n + 1 holds

A9 * (i,j) = 0. F

S

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. F_{1}()

n <= n + 1
by NAT_1:13;A9 * (i,j) = 0. F

let i, j be Nat; :: thesis: ( [i,j] in Indices A9 & i > len f & j <= n + 1 implies A9 * (i,j) = 0. F_{1}() )

assume that

A18: ( [i,j] in Indices A9 & i > len f ) and

A19: j <= n + 1 ; :: thesis: A9 * (i,j) = 0. F_{1}()

( j <= n or j = n + 1 ) by A19, NAT_1:8;

hence A9 * (i,j) = 0. F_{1}()
by A10, A16, A18; :: thesis: verum

end;assume that

A18: ( [i,j] in Indices A9 & i > len f ) and

A19: j <= n + 1 ; :: thesis: A9 * (i,j) = 0. F

( j <= n or j = n + 1 ) by A19, NAT_1:8;

hence A9 * (i,j) = 0. F

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 A12, NAT_1:12;

hence ex A9 being Matrix of F

( P

( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n + 1 holds

A9 * (i,j) = 0. F

S

suppose
ex i, j being Nat st

( [i,j] in Indices A9 & i > len f & j = n + 1 & A9 * (i,j) <> 0. F_{1}() )
; :: thesis: ex A9 being Matrix of F_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = 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. F_{1}() ) & f is one-to-one & len f <= n + 1 & len f <= F_{2}() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds

S_{1}[f,i,j,A9] ) ) )

( [i,j] in Indices A9 & i > len f & j = n + 1 & A9 * (i,j) <> 0. F

( P

( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n + 1 holds

A9 * (i,j) = 0. F

S

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. F_{1}()
;

A25: Indices A9 = [:(Seg F_{2}()),(Seg F_{3}()):]
by A4, MATRIX_0:23;

then A26: n + 1 in Seg F_{3}()
by A21, A23, ZFMISC_1:87;

A27: i0 in Seg F_{2}()
by A21, A25, ZFMISC_1:87;

then A28: i0 <= F_{2}()
by FINSEQ_1:1;

A29: (len f) + 1 <= i0 by A22, NAT_1:13;

then ( 0 + 1 <= (len f) + 1 & (len f) + 1 <= F_{2}() )
by A28, XREAL_1:7, XXREAL_0:2;

then A30: (len f) + 1 in Seg F_{2}()
;

defpred S_{3}[ Nat] means ( $1 <= F_{2}() implies ex A9 being Matrix of F_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F_{1}() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds

A9 * (i,j) = 0. F_{1}() ) & ( for i, j being Nat st i in dom f holds

S_{1}[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= $1 holds

A9 * (j,(n + 1)) = 0. F_{1}() ) ) );

A31: dom f = Seg (len f) by FINSEQ_1:def 3;

n <= F_{3}()
by A7, NAT_1:13;

then A32: Seg n c= Seg F_{3}()
by FINSEQ_1:5;

A33: Seg (len f) c= Seg F_{2}()
by A13, FINSEQ_1:5;

A34: for k being Nat st S_{3}[k] holds

S_{3}[k + 1]
_{3}()
by A21, A25, ZFMISC_1:87;

ex A9 being Matrix of F_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F_{1}() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds

A9 * (i,j) = 0. F_{1}() ) & ( for i, j being Nat st i in dom f holds

S_{1}[f,i,j,A9] ) )
_{2}(),F_{3}(),F_{1}(), B0 being Matrix of F_{2}(),F_{4}(),F_{1}() such that

A114: ( P_{1}[A0,B0] & the_rank_of F_{5}() = the_rank_of A0 & A0 * (((len f) + 1),(n + 1)) <> 0. F_{1}() & ( for i, j being Nat st [i,j] in Indices A0 & i > len f & j <= n holds

A0 * (i,j) = 0. F_{1}() ) & ( for i, j being Nat st i in dom f holds

S_{1}[f,i,j,A0] ) )
;

A115: S_{3}[ 0 ]
_{3}[k]
from NAT_1:sch 2(A115, A34);

then consider Aa being Matrix of F_{2}(),F_{3}(),F_{1}(), Bb being Matrix of F_{2}(),F_{4}(),F_{1}() such that

A117: ( P_{1}[Aa,Bb] & the_rank_of F_{5}() = the_rank_of Aa )
and

A118: Aa * (((len f) + 1),(n + 1)) <> 0. F_{1}()
and

A119: for i, j being Nat st [i,j] in Indices Aa & i > len f & j <= n holds

Aa * (i,j) = 0. F_{1}()
and

A120: for i, j being Nat st i in dom f holds

S_{1}[f,i,j,Aa]
and

A121: for j being Nat st j in (dom Aa) \ {((len f) + 1)} & j <= F_{2}() holds

Aa * (j,(n + 1)) = 0. F_{1}()
;

take Aa ; :: thesis: ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[Aa,B9] & the_rank_of F_{5}() = 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_{1}() ) & f is one-to-one & len f <= n + 1 & len f <= F_{2}() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds

S_{1}[f,i,j,Aa] ) ) )

take Bb ; :: thesis: ( P_{1}[Aa,Bb] & the_rank_of F_{5}() = 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_{1}() ) & f is one-to-one & len f <= n + 1 & len f <= F_{2}() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds

S_{1}[f,i,j,Aa] ) ) )

thus ( P_{1}[Aa,Bb] & the_rank_of F_{5}() = 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_{1}() ) & f is one-to-one & len f <= n + 1 & len f <= F_{2}() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds

S_{1}[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. F_{1}() ) & f9 is one-to-one & len f9 <= n + 1 & len f9 <= F_{2}() & rng f9 c= Seg (n + 1) & ( for i, j being Nat st i in dom f9 holds

S_{1}[f9,i,j,Aa] ) )

A122: len f9 = (len f) + 1 by FINSEQ_2:16;

A123: ( len Aa = F_{2}() & dom Aa = Seg (len Aa) )
by A4, FINSEQ_1:def 3, MATRIX_0:23;

_{3}()
by A4, MATRIX_0:23;

A131: len f9 <= F_{2}()
by A28, A29, A122, XXREAL_0:2;

A173: (Seg n) \/ {(n + 1)} = Seg (n + 1) by FINSEQ_1:9;

( rng f misses {(n + 1)} & <*(n + 1)*> is one-to-one ) by A14, FINSEQ_3:14, XBOOLE_1:63;

hence ( ( for i, j being Nat st [i,j] in Indices Aa & i > len f9 & j <= n + 1 holds

Aa * (i,j) = 0. F_{1}() ) & f9 is one-to-one & len f9 <= n + 1 & len f9 <= F_{2}() & rng f9 c= Seg (n + 1) & ( for i, j being Nat st i in dom f9 holds

S_{1}[f9,i,j,Aa] ) )
by A11, A12, A28, A29, A122, A124, A172, A173, A132, FINSEQ_1:31, FINSEQ_3:91, XREAL_1:6, XXREAL_0:2; :: thesis: verum

end;A21: [i0,j0] in Indices A9 and

A22: i0 > len f and

A23: j0 = n + 1 and

A24: A9 * (i0,j0) <> 0. F

A25: Indices A9 = [:(Seg F

then A26: n + 1 in Seg F

A27: i0 in Seg F

then A28: i0 <= F

A29: (len f) + 1 <= i0 by A22, NAT_1:13;

then ( 0 + 1 <= (len f) + 1 & (len f) + 1 <= F

then A30: (len f) + 1 in Seg F

defpred S

( P

A9 * (i,j) = 0. F

S

A9 * (j,(n + 1)) = 0. F

A31: dom f = Seg (len f) by FINSEQ_1:def 3;

n <= F

then A32: Seg n c= Seg F

A33: Seg (len f) c= Seg F

A34: for k being Nat st S

S

proof

A90:
j0 in Seg F
let k be Nat; :: thesis: ( S_{3}[k] implies S_{3}[k + 1] )

assume A35: S_{3}[k]
; :: thesis: S_{3}[k + 1]

set k1 = k + 1;

assume k + 1 <= F_{2}()
; :: thesis: ex A9 being Matrix of F_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F_{1}() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds

A9 * (i,j) = 0. F_{1}() ) & ( for i, j being Nat st i in dom f holds

S_{1}[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. F_{1}() ) )

then consider AA being Matrix of F_{2}(),F_{3}(),F_{1}(), BB being Matrix of F_{2}(),F_{4}(),F_{1}() such that

A36: P_{1}[AA,BB]
and

A37: the_rank_of F_{5}() = the_rank_of AA
and

A38: AA * (((len f) + 1),(n + 1)) <> 0. F_{1}()
and

A39: for i, j being Nat st [i,j] in Indices AA & i > len f & j <= n holds

AA * (i,j) = 0. F_{1}()
and

A40: for i, j being Nat st i in dom f holds

S_{1}[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_{1}()
by A35, NAT_1:13;

_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F_{1}() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds

A9 * (i,j) = 0. F_{1}() ) & ( for i, j being Nat st i in dom f holds

S_{1}[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. F_{1}() ) )
; :: thesis: verum

end;assume A35: S

set k1 = k + 1;

assume k + 1 <= F

( P

A9 * (i,j) = 0. F

S

A9 * (j,(n + 1)) = 0. F

then consider AA being Matrix of F

A36: P

A37: the_rank_of F

A38: AA * (((len f) + 1),(n + 1)) <> 0. F

A39: for i, j being Nat st [i,j] in Indices AA & i > len f & j <= n holds

AA * (i,j) = 0. F

A40: for i, j being Nat st i in dom f holds

S

A41: for j being Nat st j in (dom AA) \ {((len f) + 1)} & j <= k holds

AA * (j,(n + 1)) = 0. F

now :: thesis: ex RA being Matrix of F_{2}(),F_{3}(),F_{1}() ex RB being Matrix of F_{2}(),F_{4}(),F_{1}() ex A9 being Matrix of F_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F_{1}() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds

A9 * (i,j) = 0. F_{1}() ) & ( for i, j being Nat st i in dom f holds

S_{1}[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. F_{1}() ) )end;

hence
ex A9 being Matrix of F( P

A9 * (i,j) = 0. F

S

A9 * (j,(n + 1)) = 0. F

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

end;

suppose A42:
k + 1 = (len f) + 1
; :: thesis: ex RA being Matrix of F_{2}(),F_{3}(),F_{1}() ex RB being Matrix of F_{2}(),F_{4}(),F_{1}() ex A9 being Matrix of F_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F_{1}() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds

A9 * (i,j) = 0. F_{1}() ) & ( for i, j being Nat st i in dom f holds

S_{1}[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. F_{1}() ) )

( P

A9 * (i,j) = 0. F

S

A9 * (j,(n + 1)) = 0. F

take RA = AA; :: thesis: ex RB being Matrix of F_{2}(),F_{4}(),F_{1}() ex A9 being Matrix of F_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F_{1}() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds

A9 * (i,j) = 0. F_{1}() ) & ( for i, j being Nat st i in dom f holds

S_{1}[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. F_{1}() ) )

take RB = BB; :: thesis: ex A9 being Matrix of F_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F_{1}() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds

A9 * (i,j) = 0. F_{1}() ) & ( for i, j being Nat st i in dom f holds

S_{1}[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. F_{1}() ) )

_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F_{1}() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds

A9 * (i,j) = 0. F_{1}() ) & ( for i, j being Nat st i in dom f holds

S_{1}[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. F_{1}() ) )
by A36, A37, A38, A39, A40; :: thesis: verum

end;( P

A9 * (i,j) = 0. F

S

A9 * (j,(n + 1)) = 0. F

take RB = BB; :: thesis: ex A9 being Matrix of F

( P

A9 * (i,j) = 0. F

S

A9 * (j,(n + 1)) = 0. F

now :: thesis: for j being Nat st j in (dom RA) \ {((len f) + 1)} & j <= k + 1 holds

RA * (j,(n + 1)) = 0. F_{1}()

hence
ex A9 being Matrix of FRA * (j,(n + 1)) = 0. F

let j be Nat; :: thesis: ( j in (dom RA) \ {((len f) + 1)} & j <= k + 1 implies RA * (j,(n + 1)) = 0. F_{1}() )

assume that

A43: j in (dom RA) \ {((len f) + 1)} and

A44: j <= k + 1 ; :: thesis: RA * (j,(n + 1)) = 0. F_{1}()

j <> (len f) + 1 by A43, ZFMISC_1:56;

then j < k + 1 by A42, A44, XXREAL_0:1;

then j <= k by NAT_1:13;

hence RA * (j,(n + 1)) = 0. F_{1}()
by A41, A43; :: thesis: verum

end;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:56;

then j < k + 1 by A42, A44, XXREAL_0:1;

then j <= k by NAT_1:13;

hence RA * (j,(n + 1)) = 0. F

( P

A9 * (i,j) = 0. F

S

A9 * (j,(n + 1)) = 0. F

suppose A45:
k + 1 <> (len f) + 1
; :: thesis: ex RA being FinSequence of the carrier of F_{1}() * ex RB being Matrix of F_{2}(),F_{4}(),F_{1}() ex A9 being Matrix of F_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F_{1}() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds

A9 * (i,j) = 0. F_{1}() ) & ( for i, j being Nat st i in dom f holds

S_{1}[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. F_{1}() ) )

( P

A9 * (i,j) = 0. F

S

A9 * (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_{3}()
by A4, MATRIX_0:23;

then A47: len ((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))) = F_{3}()
by CARD_1:def 7;

A48: Indices A9 = Indices AA by MATRIX_0:26;

then [((len f) + 1),(n + 1)] in Indices AA by A25, A30, A26, ZFMISC_1:87;

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_{1}()
by A38, A45, A46, A47, MATRIX11:def 3;

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;

_{7}(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 F_{2}(),F_{4}(),F_{1}() ex A9 being Matrix of F_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F_{1}() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds

A9 * (i,j) = 0. F_{1}() ) & ( for i, j being Nat st i in dom f holds

S_{1}[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. F_{1}() ) )

take RB = F_{7}(BB,(k + 1),((len f) + 1),(- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) ")))); :: thesis: ex A9 being Matrix of F_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F_{1}() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds

A9 * (i,j) = 0. F_{1}() ) & ( for i, j being Nat st i in dom f holds

S_{1}[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. F_{1}() ) )

A58: width RA = F_{3}()
by A4, MATRIX_0:23;

A59: len AA = F_{2}()
by MATRIX_0:def 2;

then A89: the_rank_of F_{5}() = the_rank_of RA
by A37, A45, MATRIX13:92;

P_{1}[RA,RB]
by A2, A36, A45, A88, A69;

hence ex A9 being Matrix of F_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F_{1}() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds

A9 * (i,j) = 0. F_{1}() ) & ( for i, j being Nat st i in dom f holds

S_{1}[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. F_{1}() ) )
by A89, A49, A51, A70, A60; :: thesis: verum

end;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

then A47: len ((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))) = F

A48: Indices A9 = Indices AA by MATRIX_0:26;

then [((len f) + 1),(n + 1)] in Indices AA by A25, A30, A26, ZFMISC_1:87;

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

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. F_{1}()

set RB = F(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

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_{1}() )

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_{1}()

_{1}()
; :: thesis: verum

end;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 :: 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_{1}()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. Fper cases
( i = k + 1 or i <> k + 1 )
;

end;

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_{1}()

A56:
j in Seg F_{3}()
by A25, A50, A52, ZFMISC_1:87;

then ( (len f) + 1 > len f & [((len f) + 1),j] in Indices A9 ) by A25, A30, NAT_1:13, ZFMISC_1:87;

then AA * (((len f) + 1),j) = 0. F_{1}()
by A39, A48, A54;

then (Line (AA,((len f) + 1))) . j = 0. F_{1}()
by A46, A56, MATRIX_0:def 7;

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_{1}())
by A46, A56, FVSUM_1:51

.= 0. F_{1}()
;

(Line (AA,(k + 1))) . j = AA * ((k + 1),j) by A46, A56, MATRIX_0:def 7

.= 0. F_{1}()
by A39, A48, A50, A52, A53, A54, A55
;

then (0. F_{1}()) + (0. F_{1}()) =
((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:18

.= (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_{1}()
by RLVECT_1:def 4; :: thesis: verum

end;then ( (len f) + 1 > len f & [((len f) + 1),j] in Indices A9 ) by A25, A30, NAT_1:13, ZFMISC_1:87;

then AA * (((len f) + 1),j) = 0. F

then (Line (AA,((len f) + 1))) . j = 0. F

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

.= 0. F

(Line (AA,(k + 1))) . j = AA * ((k + 1),j) by A46, A56, MATRIX_0:def 7

.= 0. F

then (0. F

.= (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

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_{1}()

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_{1}()
by A39, A48, A50, A52, A53, A54
;

:: thesis: verum

end;.= 0. F

:: thesis: verum

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 F

( P

A9 * (i,j) = 0. F

S

A9 * (j,(n + 1)) = 0. F

take RB = F

( P

A9 * (i,j) = 0. F

S

A9 * (j,(n + 1)) = 0. F

A58: width RA = F

A59: len AA = F

A60: now :: thesis: for j being Nat st j in (dom RA) \ {((len f) + 1)} & j <= k + 1 holds

RA * (j,(n + 1)) = 0. F_{1}()

A69:
dom AA = Seg (len AA)
by FINSEQ_1:def 3;RA * (j,(n + 1)) = 0. F

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_{1}() )

assume that

A62: j in (dom RA) \ {((len f) + 1)} and

A63: j <= k + 1 ; :: thesis: RA * (j,(n + 1)) = 0. F_{1}()

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:87;

A65: ( dom RA = Seg (len RA) & len RA = F_{2}() )
by FINSEQ_1:def 3, MATRIX_0:def 2;

_{1}()
; :: thesis: verum

end;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:87;

A65: ( dom RA = Seg (len RA) & len RA = F

now :: thesis: RA * (j,(n + 1)) = 0. F_{1}()end;

hence
RA * (j,(n + 1)) = 0. Fper cases
( j <= k or j = k + 1 )
by A63, NAT_1:8;

end;

suppose A66:
j <= k
; :: thesis: RA * (j,(n + 1)) = 0. F_{1}()

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_{1}()
by A41, A59, A62, A65, A61, A66
;

:: thesis: verum

end;hence RA * (j,(n + 1)) = AA * (j,(n + 1)) by A46, A47, A64, MATRIX11:def 3

.= 0. F

:: thesis: verum

suppose A67:
j = k + 1
; :: thesis: RA * (j,(n + 1)) = 0. F_{1}()

(Line (AA,((len f) + 1))) . (n + 1) = AA * (((len f) + 1),(n + 1))
by A26, A46, MATRIX_0:def 7;

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:51

.= ((- (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_ F_{1}())
by A38, VECTSP_1:def 10

.= - (AA * ((k + 1),(n + 1))) ;

(Line (AA,(k + 1))) . (n + 1) = AA * ((k + 1),(n + 1)) by A26, A46, MATRIX_0:def 7;

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:18

.= 0. F_{1}()
by VECTSP_1:19
;

hence RA * (j,(n + 1)) = 0. F_{1}()
by A46, A47, A64, A67, MATRIX11:def 3; :: thesis: verum

end;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:51

.= ((- (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_ F

.= - (AA * ((k + 1),(n + 1))) ;

(Line (AA,(k + 1))) . (n + 1) = AA * ((k + 1),(n + 1)) by A26, A46, MATRIX_0:def 7;

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:18

.= 0. F

hence RA * (j,(n + 1)) = 0. F

A70: now :: thesis: for i, j being Nat st i in dom f holds

( RA * (i,(f /. i)) <> 0. F_{1}() & ( j in dom f & i < j implies f /. i < f /. j ) & ( j in (dom f) \ {i} implies RA * (j,(f /. i)) = 0. F_{1}() ) & ( j in Seg (width RA) & j < f /. i implies RA * (i,j) = 0. F_{1}() ) )

A88:
(len f) + 1 in Seg (len AA)
by A4, A30, MATRIX_0:23;( RA * (i,(f /. i)) <> 0. F

let i, j be Nat; :: thesis: ( i in dom f implies ( RA * (i,(f /. i)) <> 0. F_{1}() & ( j in dom f & i < j implies f /. i < f /. j ) & ( j in (dom f) \ {i} implies RA * (j,(f /. i)) = 0. F_{1}() ) & ( j in Seg (width RA) & j < f /. i implies RA * (i,j) = 0. F_{1}() ) ) )

assume A71: i in dom f ; :: thesis: ( RA * (i,(f /. i)) <> 0. F_{1}() & ( j in dom f & i < j implies f /. i < f /. j ) & ( j in (dom f) \ {i} implies RA * (j,(f /. i)) = 0. F_{1}() ) & ( j in Seg (width RA) & j < f /. i implies RA * (i,j) = 0. F_{1}() ) )

set fi = f /. i;

A72: ( f /. i = f . i & f . i in rng f ) by A71, FUNCT_1:def 3, PARTFUN1:def 6;

then A73: f /. i in Seg n by A14;

A74: ( (len f) + 1 > len f & f /. i <= n ) by A14, A72, FINSEQ_1:1, 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_0:def 7, ZFMISC_1:87;

then (Line (AA,((len f) + 1))) . (f /. i) = 0. F_{1}()
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_{1}())
by A32, A46, A73, FVSUM_1:51

.= 0. F_{1}()
;

(Line (AA,(k + 1))) . (f /. i) = AA * ((k + 1),(f /. i)) by A32, A46, A73, MATRIX_0:def 7;

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_{1}())
by A32, A46, A73, A75, FVSUM_1:18

.= AA * ((k + 1),(f /. i)) by RLVECT_1:def 4 ;

A77: [i,(f /. i)] in Indices AA by A25, A32, A33, A31, A48, A71, A73, ZFMISC_1:87;

_{1}() & ( 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_{1}() ) & ( j in Seg (width RA) & j < f /. i implies RA * (i,j) = 0. F_{1}() ) )

thus ( j in (dom f) \ {i} implies RA * (j,(f /. i)) = 0. F_{1}() )
:: thesis: ( j in Seg (width RA) & j < f /. i implies RA * (i,j) = 0. F_{1}() )_{1}() )
:: thesis: verum

end;assume A71: i in dom f ; :: thesis: ( RA * (i,(f /. i)) <> 0. F

set fi = f /. i;

A72: ( f /. i = f . i & f . i in rng f ) by A71, FUNCT_1:def 3, PARTFUN1:def 6;

then A73: f /. i in Seg n by A14;

A74: ( (len f) + 1 > len f & f /. i <= n ) by A14, A72, FINSEQ_1:1, 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_0:def 7, ZFMISC_1:87;

then (Line (AA,((len f) + 1))) . (f /. i) = 0. F

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

.= 0. F

(Line (AA,(k + 1))) . (f /. i) = AA * ((k + 1),(f /. i)) by A32, A46, A73, MATRIX_0:def 7;

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

.= AA * ((k + 1),(f /. i)) by RLVECT_1:def 4 ;

A77: [i,(f /. i)] in Indices AA by A25, A32, A33, A31, A48, A71, A73, ZFMISC_1:87;

now :: thesis: RA * (i,(f /. i)) <> 0. F_{1}()

hence
( RA * (i,(f /. i)) <> 0. Fend;

thus ( j in (dom f) \ {i} implies RA * (j,(f /. i)) = 0. F

proof

thus
( j in Seg (width RA) & j < f /. i implies RA * (i,j) = 0. F
assume A78:
j in (dom f) \ {i}
; :: thesis: RA * (j,(f /. i)) = 0. F_{1}()

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:87;

end;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:87;

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

end;

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

hence RA * (j,(f /. i)) =
AA * (j,(f /. i))
by A46, A47, A79, MATRIX11:def 3

.= 0. F_{1}()
by A40, A71, A78
;

:: thesis: verum

end;.= 0. F

:: thesis: verum

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

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_{1}()
by A40, A71, A76, A78, A80
;

:: thesis: verum

end;.= 0. F

:: thesis: verum

proof

assume that

A81: j in Seg (width RA) and

A82: j < f /. i ; :: thesis: RA * (i,j) = 0. F_{1}()

A83: [((len f) + 1),j] in Indices AA by A30, A59, A69, A46, A58, A81, ZFMISC_1:87;

A84: [i,j] in Indices AA by A33, A31, A59, A69, A46, A58, A71, A81, ZFMISC_1:87;

end;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:87;

A84: [i,j] in Indices AA by A33, A31, A59, A69, A46, A58, A71, A81, ZFMISC_1:87;

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

end;

suppose
i <> k + 1
; :: thesis: RA * (i,j) = 0. F_{1}()

hence RA * (i,j) =
AA * (i,j)
by A46, A47, A84, MATRIX11:def 3

.= 0. F_{1}()
by A40, A46, A58, A71, A81, A82
;

:: thesis: verum

end;.= 0. F

:: thesis: verum

suppose A85:
i = k + 1
; :: thesis: RA * (i,j) = 0. F_{1}()

f /. i <= n
by A14, A72, FINSEQ_1:1;

then A86: j <= n by A82, XXREAL_0:2;

(len f) + 1 > len f by NAT_1:13;

then 0. F_{1}() =
AA * (((len f) + 1),j)
by A39, A83, A86

.= (Line (AA,((len f) + 1))) . j by A46, A58, A81, MATRIX_0:def 7 ;

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_{1}())
by A46, A58, A81, FVSUM_1:51

.= 0. F_{1}()
;

(Line (AA,(k + 1))) . j = AA * (i,j) by A46, A58, A81, A85, MATRIX_0:def 7

.= 0. F_{1}()
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_{1}()) + (0. F_{1}())
by A46, A58, A81, A87, FVSUM_1:18

.= 0. F_{1}()
by RLVECT_1:def 4
;

hence RA * (i,j) = 0. F_{1}()
by A46, A47, A84, A85, MATRIX11:def 3; :: thesis: verum

end;then A86: j <= n by A82, XXREAL_0:2;

(len f) + 1 > len f by NAT_1:13;

then 0. F

.= (Line (AA,((len f) + 1))) . j by A46, A58, A81, MATRIX_0:def 7 ;

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

.= 0. F

(Line (AA,(k + 1))) . j = AA * (i,j) by A46, A58, A81, A85, MATRIX_0:def 7

.= 0. F

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

hence RA * (i,j) = 0. F

then A89: the_rank_of F

P

hence ex A9 being Matrix of F

( P

A9 * (i,j) = 0. F

S

A9 * (j,(n + 1)) = 0. F

( P

A9 * (i,j) = 0. F

S

A9 * (j,(n + 1)) = 0. F

ex A9 being Matrix of F

( P

A9 * (i,j) = 0. F

S

proof
end;

then consider A0 being Matrix of Fper cases
( A9 * (((len f) + 1),(n + 1)) <> 0. F_{1}() or A9 * (((len f) + 1),(n + 1)) = 0. F_{1}() )
;

end;

suppose
A9 * (((len f) + 1),(n + 1)) <> 0. F_{1}()
; :: thesis: ex A9 being Matrix of F_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F_{1}() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds

A9 * (i,j) = 0. F_{1}() ) & ( for i, j being Nat st i in dom f holds

S_{1}[f,i,j,A9] ) )

( P

A9 * (i,j) = 0. F

S

hence
ex A9 being Matrix of F_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F_{1}() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds

A9 * (i,j) = 0. F_{1}() ) & ( for i, j being Nat st i in dom f holds

S_{1}[f,i,j,A9] ) )
by A8, A10, A15; :: thesis: verum

end;( P

A9 * (i,j) = 0. F

S

suppose A91:
A9 * (((len f) + 1),(n + 1)) = 0. F_{1}()
; :: thesis: ex A9 being Matrix of F_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F_{1}() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds

A9 * (i,j) = 0. F_{1}() ) & ( for i, j being Nat st i in dom f holds

S_{1}[f,i,j,A9] ) )

( P

A9 * (i,j) = 0. F

S

set RB = F_{7}(B9,((len f) + 1),i0,(1_ F_{1}()));

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_ F_{1}()) * (Line (A9,i0)))));

take RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))
; :: thesis: ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[ RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0))))),B9] & the_rank_of F_{5}() = the_rank_of (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) & (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (((len f) + 1),(n + 1)) <> 0. F_{1}() & ( for i, j being Nat st [i,j] in Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) & i > len f & j <= n holds

(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (i,j) = 0. F_{1}() ) & ( for i, j being Nat st i in dom f holds

S_{1}[f,i,j, RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))] ) )

take F_{7}(B9,((len f) + 1),i0,(1_ F_{1}()))
; :: thesis: ( P_{1}[ RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0))))),F_{7}(B9,((len f) + 1),i0,(1_ F_{1}()))] & the_rank_of F_{5}() = the_rank_of (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) & (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (((len f) + 1),(n + 1)) <> 0. F_{1}() & ( for i, j being Nat st [i,j] in Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) & i > len f & j <= n holds

(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (i,j) = 0. F_{1}() ) & ( for i, j being Nat st i in dom f holds

S_{1}[f,i,j, RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))] ) )

( i0 in dom A9 & dom A9 = Seg (len A9) ) by A21, FINSEQ_1:def 3, ZFMISC_1:87;

hence ( P_{1}[ RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0))))),F_{7}(B9,((len f) + 1),i0,(1_ F_{1}()))] & the_rank_of F_{5}() = the_rank_of (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) )
by A2, A8, A23, A24, A91, MATRIX13:92; :: thesis: ( (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (((len f) + 1),(n + 1)) <> 0. F_{1}() & ( for i, j being Nat st [i,j] in Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) & i > len f & j <= n holds

(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (i,j) = 0. F_{1}() ) & ( for i, j being Nat st i in dom f holds

S_{1}[f,i,j, RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))] ) )

A92: ( (1_ F_{1}()) * (Line (A9,i0)) = Line (A9,i0) & len ((Line (A9,((len f) + 1))) + (Line (A9,i0))) = width A9 )
by CARD_1:def 7, FVSUM_1:57;

[((len f) + 1),j0] in Indices A9 by A25, A30, A90, ZFMISC_1:87;

then A93: (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (((len f) + 1),(n + 1)) = ((Line (A9,((len f) + 1))) + (Line (A9,i0))) . (n + 1)
by A23, A92, MATRIX11:def 3;

A94: width A9 = F_{3}()
by A4, MATRIX_0:23;

then A95: (Line (A9,i0)) . (n + 1) = A9 * (i0,(n + 1)) by A23, A90, MATRIX_0:def 7;

(Line (A9,((len f) + 1))) . (n + 1) = 0. F_{1}()
by A23, A90, A91, A94, MATRIX_0:def 7;

then (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (((len f) + 1),(n + 1)) =
(0. F_{1}()) + (A9 * (i0,(n + 1)))
by A26, A94, A93, A95, FVSUM_1:18

.= A9 * (i0,(n + 1)) by RLVECT_1:def 4 ;

hence (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (((len f) + 1),(n + 1)) <> 0. F_{1}()
by A23, A24; :: thesis: ( ( for i, j being Nat st [i,j] in Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) & i > len f & j <= n holds

(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (i,j) = 0. F_{1}() ) & ( for i, j being Nat st i in dom f holds

S_{1}[f,i,j, RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))] ) )

A96: Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) = Indices A9
by MATRIX_0:26;

_{1}()) * (Line (A9,i0)))))) & i > len f & j <= n holds

(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (i,j) = 0. F_{1}()
; :: thesis: for i, j being Nat st i in dom f holds

S_{1}[f,i,j, RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))]

let i, j be Nat; :: thesis: ( i in dom f implies S_{1}[f,i,j, RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))] )

assume A105: i in dom f ; :: thesis: S_{1}[f,i,j, RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))]

i <= len f by A31, A105, FINSEQ_1:1;

then A106: i < (len f) + 1 by NAT_1:13;

( f /. i = f . i & f . i in rng f ) by A105, FUNCT_1:def 3, PARTFUN1:def 6;

then A107: f /. i in Seg n by A14;

then [i,(f /. i)] in Indices A9 by A25, A32, A33, A31, A105, ZFMISC_1:87;

then (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (i,(f /. i)) = A9 * (i,(f /. i))
by A92, A106, MATRIX11:def 3;

hence ( (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (i,(f /. i)) <> 0. F_{1}() & ( j in dom f & i < j implies f /. i < f /. j ) )
by A15, A105; :: thesis: ( ( j in (dom f) \ {i} implies (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (j,(f /. i)) = 0. F_{1}() ) & ( j in Seg (width (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0))))))) & j < f /. i implies (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (i,j) = 0. F_{1}() ) )

thus ( j in (dom f) \ {i} implies (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (j,(f /. i)) = 0. F_{1}() )
:: thesis: ( j in Seg (width (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0))))))) & j < f /. i implies (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (i,j) = 0. F_{1}() )

A111: j in Seg (width (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))))
and

A112: j < f /. i ; :: thesis: (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (i,j) = 0. F_{1}()

A113: width (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) = width A9
by A92, MATRIX11:def 3;

then [i,j] in Indices A9 by A25, A33, A31, A94, A105, A111, ZFMISC_1:87;

hence (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (i,j) =
A9 * (i,j)
by A92, A106, MATRIX11:def 3

.= 0. F_{1}()
by A15, A105, A111, A112, A113
;

:: thesis: verum

end;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_ F

take RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F

( P

(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F

S

take F

(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F

S

( i0 in dom A9 & dom A9 = Seg (len A9) ) by A21, FINSEQ_1:def 3, ZFMISC_1:87;

hence ( P

(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F

S

A92: ( (1_ F

[((len f) + 1),j0] in Indices A9 by A25, A30, A90, ZFMISC_1:87;

then A93: (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F

A94: width A9 = F

then A95: (Line (A9,i0)) . (n + 1) = A9 * (i0,(n + 1)) by A23, A90, MATRIX_0:def 7;

(Line (A9,((len f) + 1))) . (n + 1) = 0. F

then (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F

.= A9 * (i0,(n + 1)) by RLVECT_1:def 4 ;

hence (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F

(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F

S

A96: Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F

now :: thesis: for i, j being Nat st [i,j] in Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) & i > len f & j <= n holds

(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (i,j) = 0. F_{1}()

hence
for i, j being Nat st [i,j] in Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F

let i, j be Nat; :: thesis: ( [i,j] in Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) & i > len f & j <= n implies (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (i,j) = 0. F_{1}() )

assume that

A97: [i,j] in Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0))))))
and

A98: i > len f and

A99: j <= n ; :: thesis: (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (i,j) = 0. F_{1}()

A100: j in Seg F_{3}()
by A94, A96, A97, ZFMISC_1:87;

A101: i >= (len f) + 1 by A98, NAT_1:13;

_{1}()) * (Line (A9,i0)))))) * (i,j) = 0. F_{1}()
; :: thesis: verum

end;assume that

A97: [i,j] in Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F

A98: i > len f and

A99: j <= n ; :: thesis: (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F

A100: j in Seg F

A101: i >= (len f) + 1 by A98, NAT_1:13;

now :: thesis: (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (i,j) = 0. F_{1}()end;

hence
(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ Fper cases
( i > (len f) + 1 or i = (len f) + 1 )
by A101, XXREAL_0:1;

end;

suppose
i > (len f) + 1
; :: thesis: (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (i,j) = 0. F_{1}()

hence (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (i,j) =
A9 * (i,j)
by A92, A96, A97, MATRIX11:def 3

.= 0. F_{1}()
by A10, A96, A97, A98, A99
;

:: thesis: verum

end;.= 0. F

:: thesis: verum

suppose A102:
i = (len f) + 1
; :: thesis: (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (i,j) = 0. F_{1}()

A103:
[i0,j] in Indices A9
by A25, A27, A100, ZFMISC_1:87;

A104: ( (Line (A9,((len f) + 1))) . j = A9 * (((len f) + 1),j) & (Line (A9,i0)) . j = A9 * (i0,j) ) by A94, A100, MATRIX_0:def 7;

(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (i,j) = ((Line (A9,((len f) + 1))) + (Line (A9,i0))) . j
by A92, A96, A97, A102, MATRIX11:def 3;

hence (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (i,j) =
(A9 * (((len f) + 1),j)) + (A9 * (i0,j))
by A94, A100, A104, FVSUM_1:18

.= (0. F_{1}()) + (A9 * (i0,j))
by A10, A96, A97, A98, A99, A102

.= (0. F_{1}()) + (0. F_{1}())
by A10, A22, A99, A103

.= 0. F_{1}()
by RLVECT_1:def 4
;

:: thesis: verum

end;A104: ( (Line (A9,((len f) + 1))) . j = A9 * (((len f) + 1),j) & (Line (A9,i0)) . j = A9 * (i0,j) ) by A94, A100, MATRIX_0:def 7;

(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F

hence (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F

.= (0. F

.= (0. F

.= 0. F

:: thesis: verum

(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F

S

let i, j be Nat; :: thesis: ( i in dom f implies S

assume A105: i in dom f ; :: thesis: S

i <= len f by A31, A105, FINSEQ_1:1;

then A106: i < (len f) + 1 by NAT_1:13;

( f /. i = f . i & f . i in rng f ) by A105, FUNCT_1:def 3, PARTFUN1:def 6;

then A107: f /. i in Seg n by A14;

then [i,(f /. i)] in Indices A9 by A25, A32, A33, A31, A105, ZFMISC_1:87;

then (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F

hence ( (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F

thus ( j in (dom f) \ {i} implies (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F

proof

assume that
assume A108:
j in (dom f) \ {i}
; :: thesis: (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (j,(f /. i)) = 0. F_{1}()

then A109: j in dom f by XBOOLE_0:def 5;

then j <= len f by A31, FINSEQ_1:1;

then A110: j < (len f) + 1 by NAT_1:13;

[j,(f /. i)] in Indices A9 by A25, A32, A33, A31, A107, A109, ZFMISC_1:87;

hence (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F_{1}()) * (Line (A9,i0)))))) * (j,(f /. i)) =
A9 * (j,(f /. i))
by A92, A110, MATRIX11:def 3

.= 0. F_{1}()
by A15, A105, A108
;

:: thesis: verum

end;then A109: j in dom f by XBOOLE_0:def 5;

then j <= len f by A31, FINSEQ_1:1;

then A110: j < (len f) + 1 by NAT_1:13;

[j,(f /. i)] in Indices A9 by A25, A32, A33, A31, A107, A109, ZFMISC_1:87;

hence (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F

.= 0. F

:: thesis: verum

A111: j in Seg (width (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F

A112: j < f /. i ; :: thesis: (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F

A113: width (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F

then [i,j] in Indices A9 by A25, A33, A31, A94, A105, A111, ZFMISC_1:87;

hence (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F

.= 0. F

:: thesis: verum

A114: ( P

A0 * (i,j) = 0. F

S

A115: S

proof

for k being Nat holds S
assume
0 <= F_{2}()
; :: thesis: ex A9 being Matrix of F_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F_{1}() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds

A9 * (i,j) = 0. F_{1}() ) & ( for i, j being Nat st i in dom f holds

S_{1}[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= 0 holds

A9 * (j,(n + 1)) = 0. F_{1}() ) )

take A0 ; :: thesis: ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A0,B9] & the_rank_of F_{5}() = the_rank_of A0 & A0 * (((len f) + 1),(n + 1)) <> 0. F_{1}() & ( for i, j being Nat st [i,j] in Indices A0 & i > len f & j <= n holds

A0 * (i,j) = 0. F_{1}() ) & ( for i, j being Nat st i in dom f holds

S_{1}[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_{1}() ) )

take B0 ; :: thesis: ( P_{1}[A0,B0] & the_rank_of F_{5}() = the_rank_of A0 & A0 * (((len f) + 1),(n + 1)) <> 0. F_{1}() & ( for i, j being Nat st [i,j] in Indices A0 & i > len f & j <= n holds

A0 * (i,j) = 0. F_{1}() ) & ( for i, j being Nat st i in dom f holds

S_{1}[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_{1}() ) )

_{1}[A0,B0] & the_rank_of F_{5}() = the_rank_of A0 & A0 * (((len f) + 1),(n + 1)) <> 0. F_{1}() & ( for i, j being Nat st [i,j] in Indices A0 & i > len f & j <= n holds

A0 * (i,j) = 0. F_{1}() ) & ( for i, j being Nat st i in dom f holds

S_{1}[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_{1}() ) )
by A114; :: thesis: verum

end;( P

A9 * (i,j) = 0. F

S

A9 * (j,(n + 1)) = 0. F

take A0 ; :: thesis: ex B9 being Matrix of F

( P

A0 * (i,j) = 0. F

S

A0 * (j,(n + 1)) = 0. F

take B0 ; :: thesis: ( P

A0 * (i,j) = 0. F

S

A0 * (j,(n + 1)) = 0. F

now :: thesis: for j being Nat st j in (dom A0) \ {((len f) + 1)} & j <= 0 holds

A0 * (j,(n + 1)) = 0. F_{1}()

hence
( PA0 * (j,(n + 1)) = 0. F

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_{1}() )

assume ( j in (dom A0) \ {((len f) + 1)} & j <= 0 ) ; :: thesis: A0 * (j,(n + 1)) = 0. F_{1}()

hence A0 * (j,(n + 1)) = 0. F_{1}()
by A116; :: thesis: verum

end;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

A0 * (i,j) = 0. F

S

A0 * (j,(n + 1)) = 0. F

then consider Aa being Matrix of F

A117: ( P

A118: Aa * (((len f) + 1),(n + 1)) <> 0. F

A119: for i, j being Nat st [i,j] in Indices Aa & i > len f & j <= n holds

Aa * (i,j) = 0. F

A120: for i, j being Nat st i in dom f holds

S

A121: for j being Nat st j in (dom Aa) \ {((len f) + 1)} & j <= F

Aa * (j,(n + 1)) = 0. F

take Aa ; :: thesis: ex B9 being Matrix of F

( P

( ( for i, j being Nat st [i,j] in Indices Aa & i > len f & j <= n + 1 holds

Aa * (i,j) = 0. F

S

take Bb ; :: thesis: ( P

( ( for i, j being Nat st [i,j] in Indices Aa & i > len f & j <= n + 1 holds

Aa * (i,j) = 0. F

S

thus ( P

( ( for i, j being Nat st [i,j] in Indices Aa & i > len f & j <= n + 1 holds

Aa * (i,j) = 0. F

S

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. F

S

A122: len f9 = (len f) + 1 by FINSEQ_2:16;

A123: ( len Aa = F

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. F_{1}()

A130:
width Aa = FAa * (i,j) = 0. F

let i, j be Nat; :: thesis: ( [i,j] in Indices Aa & i > len f9 & j <= n + 1 implies Aa * (b_{1},b_{2}) = 0. F_{1}() )

assume that

A125: [i,j] in Indices Aa and

A126: i > len f9 and

A127: j <= n + 1 ; :: thesis: Aa * (b_{1},b_{2}) = 0. F_{1}()

end;assume that

A125: [i,j] in Indices Aa and

A126: i > len f9 and

A127: j <= n + 1 ; :: thesis: Aa * (b

A131: len f9 <= F

A132: now :: thesis: for i, j being Nat st i in dom f9 holds

( Aa * (i,(f9 /. i)) <> 0. F_{1}() & ( j in dom f9 & i < j implies f9 /. i < f9 /. j ) & ( j in (dom f9) \ {i} implies Aa * (j,(f9 /. i)) = 0. F_{1}() ) & ( j in Seg (width Aa) & j < f9 /. i implies Aa * (i,j) = 0. F_{1}() ) )

A172:
( rng <*(n + 1)*> = {(n + 1)} & (rng f) \/ {(n + 1)} c= (Seg n) \/ {(n + 1)} )
by A14, FINSEQ_1:38, XBOOLE_1:9;( Aa * (i,(f9 /. i)) <> 0. F

let i, j be Nat; :: thesis: ( i in dom f9 implies ( Aa * (i,(f9 /. i)) <> 0. F_{1}() & ( j in dom f9 & i < j implies f9 /. i < f9 /. j ) & ( j in (dom f9) \ {i} implies Aa * (j,(f9 /. i)) = 0. F_{1}() ) & ( j in Seg (width Aa) & j < f9 /. i implies Aa * (i,j) = 0. F_{1}() ) ) )

assume A133: i in dom f9 ; :: thesis: ( Aa * (i,(f9 /. i)) <> 0. F_{1}() & ( j in dom f9 & i < j implies f9 /. i < f9 /. j ) & ( j in (dom f9) \ {i} implies Aa * (j,(f9 /. i)) = 0. F_{1}() ) & ( j in Seg (width Aa) & j < f9 /. i implies Aa * (i,j) = 0. F_{1}() ) )

A134: dom f9 = Seg ((len f) + 1) by A122, FINSEQ_1:def 3

.= (dom f) \/ {((len f) + 1)} by A31, FINSEQ_1:9 ;

_{1}()
; :: thesis: ( ( j in dom f9 & i < j implies f9 /. i < f9 /. j ) & ( j in (dom f9) \ {i} implies Aa * (j,(f9 /. i)) = 0. F_{1}() ) & ( j in Seg (width Aa) & j < f9 /. i implies Aa * (i,j) = 0. F_{1}() ) )

thus ( j in dom f9 & i < j implies f9 /. i < f9 /. j ) :: thesis: ( ( j in (dom f9) \ {i} implies Aa * (j,(f9 /. i)) = 0. F_{1}() ) & ( j in Seg (width Aa) & j < f9 /. i implies Aa * (i,j) = 0. F_{1}() ) )

then A148: dom f9 c= dom Aa by A123, A131, FINSEQ_1:5;

thus ( j in (dom f9) \ {i} implies Aa * (j,(f9 /. i)) = 0. F_{1}() )
:: thesis: ( j in Seg (width Aa) & j < f9 /. i implies Aa * (i,j) = 0. F_{1}() )_{1}() )
:: thesis: verum

end;assume A133: i in dom f9 ; :: thesis: ( Aa * (i,(f9 /. i)) <> 0. F

A134: dom f9 = Seg ((len f) + 1) by A122, FINSEQ_1:def 3

.= (dom f) \/ {((len f) + 1)} by A31, FINSEQ_1:9 ;

A135: now :: thesis: for k being Nat st k in dom f holds

f /. k = f9 /. k

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 A134, A136, XBOOLE_0:def 3;

thus f /. k = f . k by A136, PARTFUN1:def 6

.= f9 . k by A136, FINSEQ_1:def 7

.= f9 /. k by A137, PARTFUN1:def 6 ; :: thesis: verum

end;assume A136: k in dom f ; :: thesis: f /. k = f9 /. k

A137: k in dom f9 by A134, A136, XBOOLE_0:def 3;

thus f /. k = f . k by A136, PARTFUN1:def 6

.= f9 . k by A136, FINSEQ_1:def 7

.= f9 /. k by A137, PARTFUN1:def 6 ; :: thesis: verum

now :: thesis: Aa * (i,(f9 /. i)) <> 0. F_{1}()

hence
Aa * (i,(f9 /. i)) <> 0. Fend;

thus ( j in dom f9 & i < j implies f9 /. i < f9 /. j ) :: thesis: ( ( j in (dom f9) \ {i} implies Aa * (j,(f9 /. i)) = 0. F

proof

dom f9 = Seg (len f9)
by FINSEQ_1:def 3;
assume that

A141: j in dom f9 and

A142: i < j ; :: thesis: f9 /. i < f9 /. j

end;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 A133, A134, A141, XBOOLE_0:def 3;

end;

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 A142, A143, TARSKI:def 1; :: thesis: verum

end;hence f9 /. i < f9 /. j by A142, A143, TARSKI:def 1; :: thesis: verum

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 A144, FUNCT_1:def 3, PARTFUN1:def 6;

then A146: f /. i <= n by A14, FINSEQ_1:1;

f9 . j = f9 /. j by A141, PARTFUN1:def 6;

then f /. i < f9 /. j by A146, A145, NAT_1:13;

hence f9 /. i < f9 /. j by A135, A144; :: thesis: verum

end;then A145: f9 . j = n + 1 by FINSEQ_1:42;

( f /. i = f . i & f . i in rng f ) by A144, FUNCT_1:def 3, PARTFUN1:def 6;

then A146: f /. i <= n by A14, FINSEQ_1:1;

f9 . j = f9 /. j by A141, PARTFUN1:def 6;

then f /. i < f9 /. j by A146, A145, NAT_1:13;

hence f9 /. i < f9 /. j by A135, A144; :: thesis: verum

then A148: dom f9 c= dom Aa by A123, A131, FINSEQ_1:5;

thus ( j in (dom f9) \ {i} implies Aa * (j,(f9 /. i)) = 0. F

proof

thus
( j in Seg (width Aa) & j < f9 /. i implies Aa * (i,j) = 0. F
assume A149:
j in (dom f9) \ {i}
; :: thesis: Aa * (j,(f9 /. i)) = 0. F_{1}()

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

end;

suppose A150:
i = (len f) + 1
; :: thesis: Aa * (j,(f9 /. i)) = 0. F_{1}()

(len f) + 1 in {((len f) + 1)}
by TARSKI:def 1;

then (len f) + 1 in dom f9 by A134, XBOOLE_0:def 3;

then A151: f9 . ((len f) + 1) = f9 /. i by A150, PARTFUN1:def 6;

A152: j in dom f9 by A149, ZFMISC_1:56;

j <> i by A149, ZFMISC_1:56;

then A153: j in (dom Aa) \ {i} by A148, A152, ZFMISC_1:56;

j <= F_{2}()
by A123, A148, A152, FINSEQ_1:1;

then Aa * (j,(n + 1)) = 0. F_{1}()
by A121, A150, A153;

hence Aa * (j,(f9 /. i)) = 0. F_{1}()
by A151, FINSEQ_1:42; :: thesis: verum

end;then (len f) + 1 in dom f9 by A134, XBOOLE_0:def 3;

then A151: f9 . ((len f) + 1) = f9 /. i by A150, PARTFUN1:def 6;

A152: j in dom f9 by A149, ZFMISC_1:56;

j <> i by A149, ZFMISC_1:56;

then A153: j in (dom Aa) \ {i} by A148, A152, ZFMISC_1:56;

j <= F

then Aa * (j,(n + 1)) = 0. F

hence Aa * (j,(f9 /. i)) = 0. F

suppose A154:
i <> (len f) + 1
; :: thesis: Aa * (j,(f9 /. i)) = 0. F_{1}()

A155:
j in dom f9
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 3, TARSKI:def 1;

A158: ( f /. i = f9 /. i & f . i = f /. i ) by A135, A154, A156, PARTFUN1:def 6, TARSKI:def 1;

then A159: 1 <= f9 /. i by A14, A157, FINSEQ_1:1;

A160: f9 /. i <= n by A14, A158, A157, FINSEQ_1:1;

n <= F_{3}()
by A7, NAT_1:13;

then f9 /. i <= F_{3}()
by A160, XXREAL_0:2;

then f9 /. i in Seg (width Aa) by A130, A159;

then A161: [j,(f9 /. i)] in Indices Aa by A148, A155, ZFMISC_1:87;

end;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 3, TARSKI:def 1;

A158: ( f /. i = f9 /. i & f . i = f /. i ) by A135, A154, A156, PARTFUN1:def 6, TARSKI:def 1;

then A159: 1 <= f9 /. i by A14, A157, FINSEQ_1:1;

A160: f9 /. i <= n by A14, A158, A157, FINSEQ_1:1;

n <= F

then f9 /. i <= F

then f9 /. i in Seg (width Aa) by A130, A159;

then A161: [j,(f9 /. i)] in Indices Aa by A148, A155, ZFMISC_1:87;

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

end;

suppose
j = (len f) + 1
; :: thesis: Aa * (j,(f9 /. i)) = 0. F_{1}()

then
j > len f
by NAT_1:13;

hence Aa * (j,(f9 /. i)) = 0. F_{1}()
by A119, A160, A161; :: thesis: verum

end;hence Aa * (j,(f9 /. i)) = 0. F

suppose A162:
j <> (len f) + 1
; :: thesis: Aa * (j,(f9 /. i)) = 0. F_{1}()

j in dom f9
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:56;

then j in (dom f) \ {i} by A162, A163, TARSKI:def 1, ZFMISC_1:56;

then Aa * (j,(f /. i)) = 0. F_{1}()
by A120, A154, A156, TARSKI:def 1;

hence Aa * (j,(f9 /. i)) = 0. F_{1}()
by A135, A154, A156, TARSKI:def 1; :: thesis: verum

end;then A163: ( j in dom f or j in {((len f) + 1)} ) by A134, XBOOLE_0:def 3;

j <> i by A149, ZFMISC_1:56;

then j in (dom f) \ {i} by A162, A163, TARSKI:def 1, ZFMISC_1:56;

then Aa * (j,(f /. i)) = 0. F

hence Aa * (j,(f9 /. i)) = 0. F

proof

assume that

A164: j in Seg (width Aa) and

A165: j < f9 /. i ; :: thesis: Aa * (i,j) = 0. F_{1}()

end;A164: j in Seg (width Aa) and

A165: j < f9 /. i ; :: thesis: Aa * (i,j) = 0. F

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

end;

suppose A166:
i in dom f
; :: thesis: Aa * (i,j) = 0. F_{1}()

then
f9 /. i = f /. i
by A135;

hence Aa * (i,j) = 0. F_{1}()
by A120, A164, A165, A166; :: thesis: verum

end;hence Aa * (i,j) = 0. F

suppose A167:
not i in dom f
; :: thesis: Aa * (i,j) = 0. F_{1}()

( 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: f9 . i = n + 1 by FINSEQ_1:42;

f9 . i = f9 /. i by A133, PARTFUN1:def 6;

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:87;

hence Aa * (i,j) = 0. F_{1}()
by A119, A170, A171; :: thesis: verum

end;then A168: i = (len f) + 1 by A167, TARSKI:def 1;

then A169: f9 . i = n + 1 by FINSEQ_1:42;

f9 . i = f9 /. i by A133, PARTFUN1:def 6;

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:87;

hence Aa * (i,j) = 0. F

A173: (Seg n) \/ {(n + 1)} = Seg (n + 1) by FINSEQ_1:9;

( rng f misses {(n + 1)} & <*(n + 1)*> is one-to-one ) by A14, FINSEQ_3:14, XBOOLE_1:63;

hence ( ( for i, j being Nat st [i,j] in Indices Aa & i > len f9 & j <= n + 1 holds

Aa * (i,j) = 0. F

S

proof

for n being Nat holds S
assume
0 <= F_{3}()
; :: thesis: ex A9 being Matrix of F_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = 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. F_{1}() ) & f is one-to-one & len f <= 0 & len f <= F_{2}() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds

S_{1}[f,i,j,A9] ) ) )

take A9 = F_{5}(); :: thesis: ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( P_{1}[A9,B9] & the_rank_of F_{5}() = 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. F_{1}() ) & f is one-to-one & len f <= 0 & len f <= F_{2}() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds

S_{1}[f,i,j,A9] ) ) )

take B9 = F_{6}(); :: thesis: ( P_{1}[A9,B9] & the_rank_of F_{5}() = 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. F_{1}() ) & f is one-to-one & len f <= 0 & len f <= F_{2}() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds

S_{1}[f,i,j,A9] ) ) )

thus ( P_{1}[A9,B9] & the_rank_of F_{5}() = 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. F_{1}() ) & f is one-to-one & len f <= 0 & len f <= F_{2}() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds

S_{1}[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. F_{1}() ) & f is one-to-one & len f <= 0 & len f <= F_{2}() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds

S_{1}[f,i,j,A9] ) )

A9 * (i,j) = 0. F_{1}() ) & f is one-to-one & len f <= 0 & len f <= F_{2}() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds

S_{1}[f,i,j,A9] ) )
; :: thesis: verum

end;( P

( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= 0 holds

A9 * (i,j) = 0. F

S

take A9 = F

( P

( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= 0 holds

A9 * (i,j) = 0. F

S

take B9 = F

( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= 0 holds

A9 * (i,j) = 0. F

S

thus ( P

( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= 0 holds

A9 * (i,j) = 0. F

S

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. F

S

now :: thesis: for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= 0 holds

A9 * (i,j) = 0. F_{1}()

hence
( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= 0 holds A9 * (i,j) = 0. F

let i, j be Nat; :: thesis: ( [i,j] in Indices A9 & i > len f & j <= 0 implies A9 * (i,j) = 0. F_{1}() )

assume that

A175: [i,j] in Indices A9 and

i > len f and

A176: j <= 0 ; :: thesis: A9 * (i,j) = 0. F_{1}()

j in Seg (width A9) by A175, ZFMISC_1:87;

hence A9 * (i,j) = 0. F_{1}()
by A176; :: thesis: verum

end;assume that

A175: [i,j] in Indices A9 and

i > len f and

A176: j <= 0 ; :: thesis: A9 * (i,j) = 0. F

j in Seg (width A9) by A175, ZFMISC_1:87;

hence A9 * (i,j) = 0. F

A9 * (i,j) = 0. F

S

then consider A9 being Matrix of F

A177: P

A178: the_rank_of F

A179: ex f being FinSequence of NAT st

( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= F

A9 * (i,j) = 0. F

S

consider f being FinSequence of NAT such that

A180: for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= F

A9 * (i,j) = 0. F

A181: f is one-to-one and

len f <= F

A182: len f <= F

A183: rng f c= Seg F

A184: for i, j being Nat st i in dom f holds

S

A185: len A9 = F

take A9 ; :: thesis: ex B9 being Matrix of F

( P

Line (A9,i) = F

( 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

S

take B9 ; :: thesis: ( P

Line (A9,i) = F

( 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

S

thus ( P

Line (A9,i) = F

( 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

S

A186: dom A9 = Seg (len A9) by FINSEQ_1:def 3;

set L = len f;

A187: Seg (len f) c= Seg F

( idseq (len f) is FinSequence of NAT & len (idseq (len f)) = len f ) by CARD_1:def 7, FINSEQ_2:48;

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. F

proof

then A192:
Product (diagonal_of_Matrix (Segm (A9,idL,F9))) <> 0. F
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. F_{1}() )

assume k in dom (diagonal_of_Matrix (Segm (A9,idL,F9))) ; :: thesis: (diagonal_of_Matrix (Segm (A9,idL,F9))) . k <> 0. F_{1}()

then A191: k in Seg (len f) by A190, FINSEQ_1:def 3;

then [k,k] in Indices (Segm (A9,idL,F9)) by A189, ZFMISC_1:87;

then (Segm (A9,idL,F9)) * (k,k) = A9 * ((idL . k),(f . k)) by MATRIX13:def 1

.= A9 * (k,(f . k)) by A191, FINSEQ_2:49

.= A9 * (k,(f /. k)) by A188, A191, PARTFUN1:def 6 ;

then (Segm (A9,idL,F9)) * (k,k) <> 0. F_{1}()
by A184, A188, A191;

hence (diagonal_of_Matrix (Segm (A9,idL,F9))) . k <> 0. F_{1}()
by A191, MATRIX_3:def 10; :: thesis: verum

end;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. F

assume k in dom (diagonal_of_Matrix (Segm (A9,idL,F9))) ; :: thesis: (diagonal_of_Matrix (Segm (A9,idL,F9))) . k <> 0. F

then A191: k in Seg (len f) by A190, FINSEQ_1:def 3;

then [k,k] in Indices (Segm (A9,idL,F9)) by A189, ZFMISC_1:87;

then (Segm (A9,idL,F9)) * (k,k) = A9 * ((idL . k),(f . k)) by MATRIX13:def 1

.= A9 * (k,(f . k)) by A191, FINSEQ_2:49

.= A9 * (k,(f /. k)) by A188, A191, PARTFUN1:def 6 ;

then (Segm (A9,idL,F9)) * (k,k) <> 0. F

hence (diagonal_of_Matrix (Segm (A9,idL,F9))) . k <> 0. F

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. F_{1}()

then
Segm (A9,idL,F9) is upper_triangular Matrix of len f,F(Segm (A9,idL,F9)) * (i,j) = 0. F

let i, j be Nat; :: thesis: ( [i,j] in Indices (Segm (A9,idL,F9)) & i > j implies (Segm (A9,idL,F9)) * (i,j) = 0. F_{1}() )

assume A193: [i,j] in Indices (Segm (A9,idL,F9)) ; :: thesis: ( i > j implies (Segm (A9,idL,F9)) * (i,j) = 0. F_{1}() )

A194: i in Seg (len f) by A189, A193, ZFMISC_1:87;

assume i > j ; :: thesis: (Segm (A9,idL,F9)) * (i,j) = 0. F_{1}()

then A195: i in (dom f) \ {j} by A188, A194, ZFMISC_1:56;

reconsider i9 = i, j9 = j as Element of NAT by ORDINAL1:def 12;

A196: j in Seg (len f) by A189, A193, ZFMISC_1:87;

thus (Segm (A9,idL,F9)) * (i,j) = A9 * ((idL . i9),(f . j9)) by A193, MATRIX13:def 1

.= A9 * (i,(f . j)) by A194, FINSEQ_2:49

.= A9 * (i,(f /. j)) by A188, A196, PARTFUN1:def 6

.= 0. F_{1}()
by A184, A188, A196, A195
; :: thesis: verum

end;assume A193: [i,j] in Indices (Segm (A9,idL,F9)) ; :: thesis: ( i > j implies (Segm (A9,idL,F9)) * (i,j) = 0. F

A194: i in Seg (len f) by A189, A193, ZFMISC_1:87;

assume i > j ; :: thesis: (Segm (A9,idL,F9)) * (i,j) = 0. F

then A195: i in (dom f) \ {j} by A188, A194, ZFMISC_1:56;

reconsider i9 = i, j9 = j as Element of NAT by ORDINAL1:def 12;

A196: j in Seg (len f) by A189, A193, ZFMISC_1:87;

thus (Segm (A9,idL,F9)) * (i,j) = A9 * ((idL . i9),(f . j9)) by A193, MATRIX13:def 1

.= A9 * (i,(f . j)) by A194, FINSEQ_2:49

.= A9 * (i,(f /. j)) by A188, A196, PARTFUN1:def 6

.= 0. F

then A197: Det (Segm (A9,idL,F9)) <> 0. F

A198: len (Segm (A9,(Seg (len f)),(Seg (width A9)))) = card (Seg (len f)) by MATRIX_0:def 2;

A199: width A9 = F

[:(rng idL),(rng F9):] c= Indices A9 by A183, A187, A185, A186, A199, ZFMISC_1:96;

then A200: the_rank_of A9 >= len f by A197, MATRIX13:76;

A201: now :: thesis: for i being Nat st i in (dom A9) \ (Seg (len f)) holds

Line (A9,i) = (width A9) |-> (0. F_{1}())

then
the_rank_of A9 = the_rank_of (Segm (A9,(Seg (len f)),(Seg (width A9))))
by A187, A185, A186, Th11;Line (A9,i) = (width A9) |-> (0. F

set w0 = (width A9) |-> (0. F_{1}());

let i be Nat; :: thesis: ( i in (dom A9) \ (Seg (len f)) implies Line (A9,i) = (width A9) |-> (0. F_{1}()) )

assume A202: i in (dom A9) \ (Seg (len f)) ; :: thesis: Line (A9,i) = (width A9) |-> (0. F_{1}())

set LA = Line (A9,i);

_{1}())) = width A9 )
by CARD_1:def 7;

hence Line (A9,i) = (width A9) |-> (0. F_{1}())
by A203; :: thesis: verum

end;let i be Nat; :: thesis: ( i in (dom A9) \ (Seg (len f)) implies Line (A9,i) = (width A9) |-> (0. F

assume A202: i in (dom A9) \ (Seg (len f)) ; :: thesis: Line (A9,i) = (width A9) |-> (0. F

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. F_{1}())) . j

( len (Line (A9,i)) = width A9 & len ((width A9) |-> (0. F(Line (A9,i)) . j = ((width A9) |-> (0. F

not i in Seg (len f)
by A202, XBOOLE_0:def 5;

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. F_{1}())) . j )

assume that

A205: 1 <= j and

A206: j <= width A9 ; :: thesis: (Line (A9,i)) . j = ((width A9) |-> (0. F_{1}())) . j

A207: j in Seg (width A9) by A205, A206;

A208: i in dom A9 by A202, XBOOLE_0:def 5;

then A209: [i,j] in Indices A9 by A207, ZFMISC_1:87;

thus (Line (A9,i)) . j = A9 * (i,j) by A207, MATRIX_0:def 7

.= 0. F_{1}()
by A180, A186, A199, A206, A208, A209, A204, FINSEQ_1:1

.= ((width A9) |-> (0. F_{1}())) . j
by A207, FINSEQ_2:57
; :: thesis: verum

end;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. F

assume that

A205: 1 <= j and

A206: j <= width A9 ; :: thesis: (Line (A9,i)) . j = ((width A9) |-> (0. F

A207: j in Seg (width A9) by A205, A206;

A208: i in dom A9 by A202, XBOOLE_0:def 5;

then A209: [i,j] in Indices A9 by A207, ZFMISC_1:87;

thus (Line (A9,i)) . j = A9 * (i,j) by A207, MATRIX_0:def 7

.= 0. F

.= ((width A9) |-> (0. F

hence Line (A9,i) = (width A9) |-> (0. F

then the_rank_of A9 <= card (Seg (len f)) by A198, MATRIX13:74;

then A210: the_rank_of A9 <= len f by FINSEQ_1:57;

then A211: the_rank_of F

thus for i being Nat st i in dom A9 & i > the_rank_of F

Line (A9,i) = F

( 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

S

proof

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
let i be Nat; :: thesis: ( i in dom A9 & i > the_rank_of F_{5}() implies Line (A9,i) = F_{3}() |-> (0. F_{1}()) )

assume that

A212: i in dom A9 and

A213: i > the_rank_of F_{5}()
; :: thesis: Line (A9,i) = F_{3}() |-> (0. F_{1}())

not i in Seg (len f) by A211, A213, FINSEQ_1:1;

then i in (dom A9) \ (Seg (len f)) by A212, XBOOLE_0:def 5;

hence Line (A9,i) = F_{3}() |-> (0. F_{1}())
by A199, A201; :: thesis: verum

end;assume that

A212: i in dom A9 and

A213: i > the_rank_of F

not i in Seg (len f) by A211, A213, FINSEQ_1:1;

then i in (dom A9) \ (Seg (len f)) by A212, XBOOLE_0:def 5;

hence Line (A9,i) = F

S

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

S

A214: P

A215: the_rank_of F

A216: for i being Nat st i in dom A9 & i > the_rank_of F

Line (A9,i) = F

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

S

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

S

not 0 in rng f by A220;

then reconsider rngf = rng f as finite without_zero Subset of NAT by A220, MEASURE6:def 2, XBOOLE_1:1;

A222: ( F

set S = Segm (A9,(Seg (card rngf)),rngf);

A223: dom f = Seg (the_rank_of F

take A9 ; :: thesis: ex B9 being Matrix of F

( N c= Seg F

A9 * (i,((Sgm N) /. i)) <> 0. F

Line (A9,i) = F

A9 * (i,j) = 0. F

take B9 ; :: thesis: ex N being finite without_zero Subset of NAT st

( N c= Seg F

A9 * (i,((Sgm N) /. i)) <> 0. F

Line (A9,i) = F

A9 * (i,j) = 0. F

take rngf ; :: thesis: ( rngf c= Seg F

A9 * (i,((Sgm rngf) /. i)) <> 0. F

Line (A9,i) = F

A9 * (i,j) = 0. F

len A9 = F

then ( width A9 = 0 or width A9 = F

then Seg (width A9) c= Seg F

hence ( rngf c= Seg F

A9 * (i,((Sgm rngf) /. i)) <> 0. F

Line (A9,i) = F

A9 * (i,j) = 0. F

dom f,rngf are_equipotent by A219, WELLORD2:def 4;

hence A224: card rngf = card (dom f) by CARD_1:5

.= card (Seg (the_rank_of F

.= the_rank_of F

:: thesis: ( P

A9 * (i,((Sgm rngf) /. i)) <> 0. F

Line (A9,i) = F

A9 * (i,j) = 0. F

now :: thesis: for i, j being Nat st i in dom f & j in dom f & i < j holds

f . i < f . j

then A227:
Sgm rngf = f
by A219, A220, Th6;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 A225, PARTFUN1:def 6;

hence f . i < f . j by A221, A225, A226; :: thesis: verum

end;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 6;

hence f . i < f . j by A221, A225, A226; :: thesis: verum

thus P

A9 * (i,((Sgm rngf) /. i)) <> 0. F

Line (A9,i) = F

A9 * (i,j) = 0. F

A228: card (Seg (card rngf)) = card rngf by FINSEQ_1:57;

then A229: Indices (Segm (A9,(Seg (card rngf)),rngf)) = [:(Seg (the_rank_of F

now :: thesis: for i, j being Nat st i in Seg (the_rank_of F_{5}()) & j in Seg (the_rank_of F_{5}()) & i <> j holds

(Segm (A9,(Seg (card rngf)),rngf)) * (i,j) = 0. F_{1}()

hence
Segm (A9,(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 (Segm (A9,(Seg (card rngf)),rngf)) * (i,j) = 0. F

let i, j be Nat; :: thesis: ( i in Seg (the_rank_of F_{5}()) & j in Seg (the_rank_of F_{5}()) & i <> j implies (Segm (A9,(Seg (card rngf)),rngf)) * (i,j) = 0. F_{1}() )

assume that

A230: i in Seg (the_rank_of F_{5}())
and

A231: j in Seg (the_rank_of F_{5}())
and

A232: i <> j ; :: thesis: (Segm (A9,(Seg (card rngf)),rngf)) * (i,j) = 0. F_{1}()

A233: i in (dom f) \ {j} by A223, A230, A232, ZFMISC_1:56;

A234: (idseq (the_rank_of F_{5}())) . i = i
by A230, FINSEQ_2:49;

[i,j] in Indices (Segm (A9,(Seg (card rngf)),rngf)) by A229, A230, A231, ZFMISC_1:87;

then (Segm (A9,(Seg (card rngf)),rngf)) * (i,j) = A9 * (((Sgm (Seg (the_rank_of F_{5}()))) . i),(f . j))
by A224, A227, MATRIX13:def 1

.= A9 * (i,(f . j)) by A234, FINSEQ_3:48

.= A9 * (i,(f /. j)) by A223, A231, PARTFUN1:def 6 ;

hence (Segm (A9,(Seg (card rngf)),rngf)) * (i,j) = 0. F_{1}()
by A221, A223, A231, A233; :: thesis: verum

end;assume that

A230: i in Seg (the_rank_of F

A231: j in Seg (the_rank_of F

A232: i <> j ; :: thesis: (Segm (A9,(Seg (card rngf)),rngf)) * (i,j) = 0. F

A233: i in (dom f) \ {j} by A223, A230, A232, ZFMISC_1:56;

A234: (idseq (the_rank_of F

[i,j] in Indices (Segm (A9,(Seg (card rngf)),rngf)) by A229, A230, A231, ZFMISC_1:87;

then (Segm (A9,(Seg (card rngf)),rngf)) * (i,j) = A9 * (((Sgm (Seg (the_rank_of F

.= A9 * (i,(f . j)) by A234, FINSEQ_3:48

.= A9 * (i,(f /. j)) by A223, A231, PARTFUN1:def 6 ;

hence (Segm (A9,(Seg (card rngf)),rngf)) * (i,j) = 0. F

A9 * (i,((Sgm rngf) /. i)) <> 0. F

Line (A9,i) = F

A9 * (i,j) = 0. F

thus for i being Nat st i in Seg (card rngf) holds

A9 * (i,((Sgm rngf) /. i)) <> 0. F

Line (A9,i) = F

A9 * (i,j) = 0. F

thus for i being Nat st i in dom A9 & i > card rngf holds

Line (A9,i) = F

A9 * (i,j) = 0. F

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. F

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. F

j < f /. i by A224, A227, A223, A235, A237, PARTFUN1:def 6;

hence A9 * (i,j) = 0. F