defpred S1[ FinSequence of NAT , Nat, Nat, Matrix of F2(),F3(),F1()] means ( $4 * ($2,($1 /. $2)) <> 0. F1() & ( $3 in dom $1 & $2 < $3 implies $1 /. $2 < $1 /. $3 ) & ( $3 in (dom $1) \ {$2} implies $4 * ($3,($1 /. $2)) = 0. F1() ) & ( $3 in Seg (width $4) & $3 < $1 /. $2 implies $4 * ($2,$3) = 0. F1() ) );
set r = the_rank_of F5();
ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ( for i being Nat st i in dom A9 & i > the_rank_of F5() holds
Line (A9,i) = F3() |-> (0. F1()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A9 & f is one-to-one & rng f c= Seg (width A9) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )
proof
per cases ( F2() = 0 or F2() > 0 ) ;
suppose A3: F2() = 0 ; :: thesis: ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ( for i being Nat st i in dom A9 & i > the_rank_of F5() holds
Line (A9,i) = F3() |-> (0. F1()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A9 & f is one-to-one & rng f c= Seg (width A9) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )
take A9 = F5(); :: thesis: ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ( for i being Nat st i in dom A9 & i > the_rank_of F5() holds
Line (A9,i) = F3() |-> (0. F1()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A9 & f is one-to-one & rng f c= Seg (width A9) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )
take B9 = F6(); :: thesis: ( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ( for i being Nat st i in dom A9 & i > the_rank_of F5() holds
Line (A9,i) = F3() |-> (0. F1()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A9 & f is one-to-one & rng f c= Seg (width A9) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )
( dom A9 = Seg (len A9) & len A9 = 0 ) by A3, FINSEQ_1:def 3, MATRIX_0:def 2;
hence ( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ( for i being Nat st i in dom A9 & i > the_rank_of F5() holds
Line (A9,i) = F3() |-> (0. F1()) ) ) by A1; :: thesis: ex f being FinSequence of NAT st
( len f = the_rank_of A9 & f is one-to-one & rng f c= Seg (width A9) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) )
take <*> NAT ; :: thesis: ( len (<*> 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
S1[ <*> 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
S1[ <*> NAT,i,j,A9] ) ) by MATRIX13:74; :: thesis: verum
end;
suppose A4: F2() > 0 ; :: thesis: ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ( for i being Nat st i in dom A9 & i > the_rank_of F5() holds
Line (A9,i) = F3() |-> (0. F1()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A9 & f is one-to-one & rng f c= Seg (width A9) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )
defpred S2[ Nat] means ( $1 <= F3() implies ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= $1 holds
A9 * (i,j) = 0. F1() ) & f is one-to-one & len f <= $1 & len f <= F2() & rng f c= Seg $1 & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) ) );
A5: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A6: S2[n] ; :: thesis: S2[n + 1]
set n1 = n + 1;
assume A7: n + 1 <= F3() ; :: thesis: ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n + 1 holds
A9 * (i,j) = 0. F1() ) & f is one-to-one & len f <= n + 1 & len f <= F2() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )
then consider A9 being Matrix of F2(),F3(),F1(), B9 being Matrix of F2(),F4(),F1() such that
A8: ( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 ) and
A9: ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & f is one-to-one & len f <= n & len f <= F2() & rng f c= Seg n & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) by 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. F1() and
A11: f is one-to-one and
A12: len f <= n and
A13: len f <= F2() and
A14: rng f c= Seg n and
A15: for i, j being Nat st i in dom f holds
S1[f,i,j,A9] by A9;
per cases ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j = n + 1 holds
A9 * (i,j) = 0. F1() or ex i, j being Nat st
( [i,j] in Indices A9 & i > len f & j = n + 1 & A9 * (i,j) <> 0. F1() ) ) ;
suppose A16: for i, j being Nat st [i,j] in Indices A9 & i > len f & j = n + 1 holds
A9 * (i,j) = 0. F1() ; :: thesis: ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n + 1 holds
A9 * (i,j) = 0. F1() ) & f is one-to-one & len f <= n + 1 & len f <= F2() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )
A17: now :: thesis: for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n + 1 holds
A9 * (i,j) = 0. F1()
let i, j be Nat; :: thesis: ( [i,j] in Indices A9 & i > len f & j <= n + 1 implies A9 * (i,j) = 0. F1() )
assume that
A18: ( [i,j] in Indices A9 & i > len f ) and
A19: j <= n + 1 ; :: thesis: A9 * (i,j) = 0. F1()
( j <= n or j = n + 1 ) by A19, NAT_1:8;
hence A9 * (i,j) = 0. F1() by A10, A16, A18; :: thesis: verum
end;
n <= n + 1 by NAT_1:13;
then Seg n c= Seg (n + 1) by FINSEQ_1:5;
then A20: rng f c= Seg (n + 1) by A14;
len f <= n + 1 by A12, NAT_1:12;
hence ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n + 1 holds
A9 * (i,j) = 0. F1() ) & f is one-to-one & len f <= n + 1 & len f <= F2() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) ) by A8, A11, A13, A15, A17, A20; :: thesis: verum
end;
suppose ex i, j being Nat st
( [i,j] in Indices A9 & i > len f & j = n + 1 & A9 * (i,j) <> 0. F1() ) ; :: thesis: ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n + 1 holds
A9 * (i,j) = 0. F1() ) & f is one-to-one & len f <= n + 1 & len f <= F2() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )
then consider i0, j0 being Nat such that
A21: [i0,j0] in Indices A9 and
A22: i0 > len f and
A23: j0 = n + 1 and
A24: A9 * (i0,j0) <> 0. F1() ;
A25: Indices A9 = [:(Seg F2()),(Seg F3()):] by A4, MATRIX_0:23;
then A26: n + 1 in Seg F3() by A21, A23, ZFMISC_1:87;
A27: i0 in Seg F2() by A21, A25, ZFMISC_1:87;
then A28: i0 <= F2() by FINSEQ_1:1;
A29: (len f) + 1 <= i0 by A22, NAT_1:13;
then ( 0 + 1 <= (len f) + 1 & (len f) + 1 <= F2() ) by A28, XREAL_1:7, XXREAL_0:2;
then A30: (len f) + 1 in Seg F2() ;
defpred S3[ Nat] means ( $1 <= F2() implies ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= $1 holds
A9 * (j,(n + 1)) = 0. F1() ) ) );
A31: dom f = Seg (len f) by FINSEQ_1:def 3;
n <= F3() by A7, NAT_1:13;
then A32: Seg n c= Seg F3() by FINSEQ_1:5;
A33: Seg (len f) c= Seg F2() by A13, FINSEQ_1:5;
A34: for k being Nat st S3[k] holds
S3[k + 1]
proof
let k be Nat; :: thesis: ( S3[k] implies S3[k + 1] )
assume A35: S3[k] ; :: thesis: S3[k + 1]
set k1 = k + 1;
assume k + 1 <= F2() ; :: thesis: ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= k + 1 holds
A9 * (j,(n + 1)) = 0. F1() ) )
then consider AA being Matrix of F2(),F3(),F1(), BB being Matrix of F2(),F4(),F1() such that
A36: P1[AA,BB] and
A37: the_rank_of F5() = the_rank_of AA and
A38: AA * (((len f) + 1),(n + 1)) <> 0. F1() and
A39: for i, j being Nat st [i,j] in Indices AA & i > len f & j <= n holds
AA * (i,j) = 0. F1() and
A40: for i, j being Nat st i in dom f holds
S1[f,i,j,AA] and
A41: for j being Nat st j in (dom AA) \ {((len f) + 1)} & j <= k holds
AA * (j,(n + 1)) = 0. F1() by A35, NAT_1:13;
now :: thesis: ex RA being Matrix of F2(),F3(),F1() ex RB being Matrix of F2(),F4(),F1() ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= k + 1 holds
A9 * (j,(n + 1)) = 0. F1() ) )
per cases ( k + 1 = (len f) + 1 or k + 1 <> (len f) + 1 ) ;
suppose A42: k + 1 = (len f) + 1 ; :: thesis: ex RA being Matrix of F2(),F3(),F1() ex RB being Matrix of F2(),F4(),F1() ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= k + 1 holds
A9 * (j,(n + 1)) = 0. F1() ) )
take RA = AA; :: thesis: ex RB being Matrix of F2(),F4(),F1() ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= k + 1 holds
A9 * (j,(n + 1)) = 0. F1() ) )
take RB = BB; :: thesis: ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= k + 1 holds
A9 * (j,(n + 1)) = 0. F1() ) )
now :: thesis: for j being Nat st j in (dom RA) \ {((len f) + 1)} & j <= k + 1 holds
RA * (j,(n + 1)) = 0. F1()
let j be Nat; :: thesis: ( j in (dom RA) \ {((len f) + 1)} & j <= k + 1 implies RA * (j,(n + 1)) = 0. F1() )
assume that
A43: j in (dom RA) \ {((len f) + 1)} and
A44: j <= k + 1 ; :: thesis: RA * (j,(n + 1)) = 0. F1()
j <> (len f) + 1 by 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. F1() by A41, A43; :: thesis: verum
end;
hence ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= k + 1 holds
A9 * (j,(n + 1)) = 0. F1() ) ) by A36, A37, A38, A39, A40; :: thesis: verum
end;
suppose A45: k + 1 <> (len f) + 1 ; :: thesis: ex RA being FinSequence of the carrier of F1() * ex RB being Matrix of F2(),F4(),F1() ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= k + 1 holds
A9 * (j,(n + 1)) = 0. F1() ) )
set LA = Line (AA,(k + 1));
set LAf = Line (AA,((len f) + 1));
set a = AA * (((len f) + 1),(n + 1));
set RA = RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))));
A46: width AA = F3() by 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))))) = F3() by CARD_1:def 7;
A48: Indices A9 = Indices AA by MATRIX_0:26;
then [((len f) + 1),(n + 1)] in Indices AA by 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. F1() 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;
A51: now :: thesis: for i, j being Nat st [i,j] in Indices (RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))))) & i > len f & j <= n holds
(RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))))) * (i,j) = 0. F1()
let i, j be Nat; :: thesis: ( [i,j] in Indices (RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))))) & i > len f & j <= n implies (RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))))) * (i,j) = 0. F1() )
assume that
A52: [i,j] in Indices (RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))))) and
A53: i > len f and
A54: j <= n ; :: thesis: (RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))))) * (i,j) = 0. F1()
now :: thesis: (RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))))) * (i,j) = 0. F1()
per cases ( i = k + 1 or i <> k + 1 ) ;
suppose A55: i = k + 1 ; :: thesis: (RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))))) * (i,j) = 0. F1()
A56: j in Seg F3() by 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. F1() by A39, A48, A54;
then (Line (AA,((len f) + 1))) . j = 0. F1() 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. F1()) by A46, A56, FVSUM_1:51
.= 0. F1() ;
(Line (AA,(k + 1))) . j = AA * ((k + 1),j) by A46, A56, MATRIX_0:def 7
.= 0. F1() by A39, A48, A50, A52, A53, A54, A55 ;
then (0. F1()) + (0. F1()) = ((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))) . j by 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. F1() by RLVECT_1:def 4; :: thesis: verum
end;
suppose i <> k + 1 ; :: thesis: (RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))))) * (i,j) = 0. F1()
hence (RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))))) * (i,j) = AA * (i,j) by A48, A50, A46, A47, A52, MATRIX11:def 3
.= 0. F1() by A39, A48, A50, A52, A53, A54 ;
:: thesis: verum
end;
end;
end;
hence (RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))))) * (i,j) = 0. F1() ; :: thesis: verum
end;
set RB = F7(BB,(k + 1),((len f) + 1),(- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))));
take RA = RLine (AA,(k + 1),((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1)))))); :: thesis: ex RB being Matrix of F2(),F4(),F1() ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= k + 1 holds
A9 * (j,(n + 1)) = 0. F1() ) )
take RB = F7(BB,(k + 1),((len f) + 1),(- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) ")))); :: thesis: ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= k + 1 holds
A9 * (j,(n + 1)) = 0. F1() ) )
A58: width RA = F3() by A4, MATRIX_0:23;
A59: len AA = F2() by MATRIX_0:def 2;
A60: now :: thesis: for j being Nat st j in (dom RA) \ {((len f) + 1)} & j <= k + 1 holds
RA * (j,(n + 1)) = 0. F1()
A61: dom AA = Seg (len AA) by FINSEQ_1:def 3;
let j be Nat; :: thesis: ( j in (dom RA) \ {((len f) + 1)} & j <= k + 1 implies RA * (j,(n + 1)) = 0. F1() )
assume that
A62: j in (dom RA) \ {((len f) + 1)} and
A63: j <= k + 1 ; :: thesis: RA * (j,(n + 1)) = 0. F1()
j in dom RA by 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 = F2() ) by FINSEQ_1:def 3, MATRIX_0:def 2;
now :: thesis: RA * (j,(n + 1)) = 0. F1()
per cases ( j <= k or j = k + 1 ) by A63, NAT_1:8;
suppose A66: j <= k ; :: thesis: RA * (j,(n + 1)) = 0. F1()
then j < k + 1 by NAT_1:13;
hence RA * (j,(n + 1)) = AA * (j,(n + 1)) by A46, A47, A64, MATRIX11:def 3
.= 0. F1() by A41, A59, A62, A65, A61, A66 ;
:: thesis: verum
end;
suppose A67: j = k + 1 ; :: thesis: RA * (j,(n + 1)) = 0. F1()
(Line (AA,((len f) + 1))) . (n + 1) = AA * (((len f) + 1),(n + 1)) by 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_ F1()) 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. F1() by VECTSP_1:19 ;
hence RA * (j,(n + 1)) = 0. F1() by A46, A47, A64, A67, MATRIX11:def 3; :: thesis: verum
end;
end;
end;
hence RA * (j,(n + 1)) = 0. F1() ; :: thesis: verum
end;
A69: dom AA = Seg (len AA) by FINSEQ_1:def 3;
A70: now :: thesis: for i, j being Nat st i in dom f holds
( RA * (i,(f /. i)) <> 0. F1() & ( j in dom f & i < j implies f /. i < f /. j ) & ( j in (dom f) \ {i} implies RA * (j,(f /. i)) = 0. F1() ) & ( j in Seg (width RA) & j < f /. i implies RA * (i,j) = 0. F1() ) )
let i, j be Nat; :: thesis: ( i in dom f implies ( RA * (i,(f /. i)) <> 0. F1() & ( j in dom f & i < j implies f /. i < f /. j ) & ( j in (dom f) \ {i} implies RA * (j,(f /. i)) = 0. F1() ) & ( j in Seg (width RA) & j < f /. i implies RA * (i,j) = 0. F1() ) ) )
assume A71: i in dom f ; :: thesis: ( RA * (i,(f /. i)) <> 0. F1() & ( j in dom f & i < j implies f /. i < f /. j ) & ( j in (dom f) \ {i} implies RA * (j,(f /. i)) = 0. F1() ) & ( j in Seg (width RA) & j < f /. i implies RA * (i,j) = 0. F1() ) )
set fi = f /. i;
A72: ( f /. i = f . i & f . i in rng f ) by 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. F1() 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. F1()) by A32, A46, A73, FVSUM_1:51
.= 0. F1() ;
(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. F1()) 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;
now :: thesis: RA * (i,(f /. i)) <> 0. F1()
per cases ( i <> k + 1 or i = k + 1 ) ;
suppose i <> k + 1 ; :: thesis: RA * (i,(f /. i)) <> 0. F1()
then RA * (i,(f /. i)) = AA * (i,(f /. i)) by A46, A47, A77, MATRIX11:def 3;
hence RA * (i,(f /. i)) <> 0. F1() by A40, A71; :: thesis: verum
end;
suppose i = k + 1 ; :: thesis: RA * (i,(f /. i)) <> 0. F1()
then RA * (i,(f /. i)) = AA * (i,(f /. i)) by A46, A47, A77, A76, MATRIX11:def 3;
hence RA * (i,(f /. i)) <> 0. F1() by A40, A71; :: thesis: verum
end;
end;
end;
hence ( RA * (i,(f /. i)) <> 0. F1() & ( 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. F1() ) & ( j in Seg (width RA) & j < f /. i implies RA * (i,j) = 0. F1() ) )
thus ( j in (dom f) \ {i} implies RA * (j,(f /. i)) = 0. F1() ) :: thesis: ( j in Seg (width RA) & j < f /. i implies RA * (i,j) = 0. F1() )
proof
assume A78: j in (dom f) \ {i} ; :: thesis: RA * (j,(f /. i)) = 0. F1()
then j in Seg (len f) by 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 ) ;
suppose j <> k + 1 ; :: thesis: RA * (j,(f /. i)) = 0. F1()
hence RA * (j,(f /. i)) = AA * (j,(f /. i)) by A46, A47, A79, MATRIX11:def 3
.= 0. F1() by A40, A71, A78 ;
:: thesis: verum
end;
suppose A80: j = k + 1 ; :: thesis: RA * (j,(f /. i)) = 0. F1()
hence RA * (j,(f /. i)) = ((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))) . (f /. i) by A46, A47, A79, MATRIX11:def 3
.= 0. F1() by A40, A71, A76, A78, A80 ;
:: thesis: verum
end;
end;
end;
thus ( j in Seg (width RA) & j < f /. i implies RA * (i,j) = 0. F1() ) :: thesis: verum
proof
assume that
A81: j in Seg (width RA) and
A82: j < f /. i ; :: thesis: RA * (i,j) = 0. F1()
A83: [((len f) + 1),j] in Indices AA by 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 ) ;
suppose i <> k + 1 ; :: thesis: RA * (i,j) = 0. F1()
hence RA * (i,j) = AA * (i,j) by A46, A47, A84, MATRIX11:def 3
.= 0. F1() by A40, A46, A58, A71, A81, A82 ;
:: thesis: verum
end;
suppose A85: i = k + 1 ; :: thesis: RA * (i,j) = 0. F1()
f /. i <= n by 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. F1() = 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. F1()) by A46, A58, A81, FVSUM_1:51
.= 0. F1() ;
(Line (AA,(k + 1))) . j = AA * (i,j) by A46, A58, A81, A85, MATRIX_0:def 7
.= 0. F1() by A40, A46, A58, A71, A81, A82 ;
then ((Line (AA,(k + 1))) + ((- ((AA * ((k + 1),(n + 1))) * ((AA * (((len f) + 1),(n + 1))) "))) * (Line (AA,((len f) + 1))))) . j = (0. F1()) + (0. F1()) by A46, A58, A81, A87, FVSUM_1:18
.= 0. F1() by RLVECT_1:def 4 ;
hence RA * (i,j) = 0. F1() by A46, A47, A84, A85, MATRIX11:def 3; :: thesis: verum
end;
end;
end;
end;
A88: (len f) + 1 in Seg (len AA) by A4, A30, MATRIX_0:23;
then A89: the_rank_of F5() = the_rank_of RA by A37, A45, MATRIX13:92;
P1[RA,RB] by A2, A36, A45, A88, A69;
hence ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= k + 1 holds
A9 * (j,(n + 1)) = 0. F1() ) ) by A89, A49, A51, A70, A60; :: thesis: verum
end;
end;
end;
hence ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= k + 1 holds
A9 * (j,(n + 1)) = 0. F1() ) ) ; :: thesis: verum
end;
A90: j0 in Seg F3() by A21, A25, ZFMISC_1:87;
ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) )
proof
per cases ( A9 * (((len f) + 1),(n + 1)) <> 0. F1() or A9 * (((len f) + 1),(n + 1)) = 0. F1() ) ;
suppose A9 * (((len f) + 1),(n + 1)) <> 0. F1() ; :: thesis: ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) )
hence ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) by A8, A10, A15; :: thesis: verum
end;
suppose A91: A9 * (((len f) + 1),(n + 1)) = 0. F1() ; :: thesis: ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) )
set RB = F7(B9,((len f) + 1),i0,(1_ F1()));
set LA = Line (A9,i0);
set LAf = Line (A9,((len f) + 1));
set RA = RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))));
take RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0))))) ; :: thesis: ex B9 being Matrix of F2(),F4(),F1() st
( P1[ RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0))))),B9] & the_rank_of F5() = the_rank_of (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) & (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) & i > len f & j <= n holds
(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j, RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))] ) )
take F7(B9,((len f) + 1),i0,(1_ F1())) ; :: thesis: ( P1[ RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0))))),F7(B9,((len f) + 1),i0,(1_ F1()))] & the_rank_of F5() = the_rank_of (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) & (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) & i > len f & j <= n holds
(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j, RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))] ) )
( i0 in dom A9 & dom A9 = Seg (len A9) ) by A21, FINSEQ_1:def 3, ZFMISC_1:87;
hence ( P1[ RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0))))),F7(B9,((len f) + 1),i0,(1_ F1()))] & the_rank_of F5() = the_rank_of (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) ) by A2, A8, A23, A24, A91, MATRIX13:92; :: thesis: ( (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) & i > len f & j <= n holds
(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j, RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))] ) )
A92: ( (1_ F1()) * (Line (A9,i0)) = Line (A9,i0) & len ((Line (A9,((len f) + 1))) + (Line (A9,i0))) = width A9 ) by 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_ F1()) * (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 = F3() 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. F1() by A23, A90, A91, A94, MATRIX_0:def 7;
then (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (((len f) + 1),(n + 1)) = (0. F1()) + (A9 * (i0,(n + 1))) by 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_ F1()) * (Line (A9,i0)))))) * (((len f) + 1),(n + 1)) <> 0. F1() 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_ F1()) * (Line (A9,i0)))))) & i > len f & j <= n holds
(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j, RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))] ) )
A96: Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) = Indices A9 by MATRIX_0:26;
now :: thesis: for i, j being Nat st [i,j] in Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) & i > len f & j <= n holds
(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1()
let i, j be Nat; :: thesis: ( [i,j] in Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) & i > len f & j <= n implies (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1() )
assume that
A97: [i,j] in Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) and
A98: i > len f and
A99: j <= n ; :: thesis: (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1()
A100: j in Seg F3() by A94, A96, A97, ZFMISC_1:87;
A101: i >= (len f) + 1 by A98, NAT_1:13;
now :: thesis: (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1()
per cases ( i > (len f) + 1 or i = (len f) + 1 ) by A101, XXREAL_0:1;
suppose i > (len f) + 1 ; :: thesis: (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1()
hence (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = A9 * (i,j) by A92, A96, A97, MATRIX11:def 3
.= 0. F1() by A10, A96, A97, A98, A99 ;
:: thesis: verum
end;
suppose A102: i = (len f) + 1 ; :: thesis: (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1()
A103: [i0,j] in Indices A9 by 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_ F1()) * (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_ F1()) * (Line (A9,i0)))))) * (i,j) = (A9 * (((len f) + 1),j)) + (A9 * (i0,j)) by A94, A100, A104, FVSUM_1:18
.= (0. F1()) + (A9 * (i0,j)) by A10, A96, A97, A98, A99, A102
.= (0. F1()) + (0. F1()) by A10, A22, A99, A103
.= 0. F1() by RLVECT_1:def 4 ;
:: thesis: verum
end;
end;
end;
hence (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1() ; :: thesis: verum
end;
hence for i, j being Nat st [i,j] in Indices (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) & i > len f & j <= n holds
(RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1() ; :: thesis: for i, j being Nat st i in dom f holds
S1[f,i,j, RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))]
let i, j be Nat; :: thesis: ( i in dom f implies S1[f,i,j, RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))] )
assume A105: i in dom f ; :: thesis: S1[f,i,j, RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))]
i <= len f by 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_ F1()) * (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_ F1()) * (Line (A9,i0)))))) * (i,(f /. i)) <> 0. F1() & ( 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_ F1()) * (Line (A9,i0)))))) * (j,(f /. i)) = 0. F1() ) & ( j in Seg (width (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0))))))) & j < f /. i implies (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1() ) )
thus ( j in (dom f) \ {i} implies (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (j,(f /. i)) = 0. F1() ) :: thesis: ( j in Seg (width (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0))))))) & j < f /. i implies (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1() )
proof
assume A108: j in (dom f) \ {i} ; :: thesis: (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (j,(f /. i)) = 0. F1()
then A109: j in dom f by XBOOLE_0:def 5;
then j <= len f by 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_ F1()) * (Line (A9,i0)))))) * (j,(f /. i)) = A9 * (j,(f /. i)) by A92, A110, MATRIX11:def 3
.= 0. F1() by A15, A105, A108 ;
:: thesis: verum
end;
assume that
A111: j in Seg (width (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0))))))) and
A112: j < f /. i ; :: thesis: (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) * (i,j) = 0. F1()
A113: width (RLine (A9,((len f) + 1),((Line (A9,((len f) + 1))) + ((1_ F1()) * (Line (A9,i0)))))) = width A9 by 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_ F1()) * (Line (A9,i0)))))) * (i,j) = A9 * (i,j) by A92, A106, MATRIX11:def 3
.= 0. F1() by A15, A105, A111, A112, A113 ;
:: thesis: verum
end;
end;
end;
then consider A0 being Matrix of F2(),F3(),F1(), B0 being Matrix of F2(),F4(),F1() such that
A114: ( P1[A0,B0] & the_rank_of F5() = the_rank_of A0 & A0 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A0 & i > len f & j <= n holds
A0 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A0] ) ) ;
A115: S3[ 0 ]
proof
assume 0 <= F2() ; :: thesis: ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & A9 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= n holds
A9 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) & ( for j being Nat st j in (dom A9) \ {((len f) + 1)} & j <= 0 holds
A9 * (j,(n + 1)) = 0. F1() ) )
take A0 ; :: thesis: ex B9 being Matrix of F2(),F4(),F1() st
( P1[A0,B9] & the_rank_of F5() = the_rank_of A0 & A0 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A0 & i > len f & j <= n holds
A0 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A0] ) & ( for j being Nat st j in (dom A0) \ {((len f) + 1)} & j <= 0 holds
A0 * (j,(n + 1)) = 0. F1() ) )
take B0 ; :: thesis: ( P1[A0,B0] & the_rank_of F5() = the_rank_of A0 & A0 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A0 & i > len f & j <= n holds
A0 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A0] ) & ( for j being Nat st j in (dom A0) \ {((len f) + 1)} & j <= 0 holds
A0 * (j,(n + 1)) = 0. F1() ) )
now :: thesis: for j being Nat st j in (dom A0) \ {((len f) + 1)} & j <= 0 holds
A0 * (j,(n + 1)) = 0. F1()
A116: dom A0 = Seg (len A0) by FINSEQ_1:def 3;
let j be Nat; :: thesis: ( j in (dom A0) \ {((len f) + 1)} & j <= 0 implies A0 * (j,(n + 1)) = 0. F1() )
assume ( j in (dom A0) \ {((len f) + 1)} & j <= 0 ) ; :: thesis: A0 * (j,(n + 1)) = 0. F1()
hence A0 * (j,(n + 1)) = 0. F1() by A116; :: thesis: verum
end;
hence ( P1[A0,B0] & the_rank_of F5() = the_rank_of A0 & A0 * (((len f) + 1),(n + 1)) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A0 & i > len f & j <= n holds
A0 * (i,j) = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A0] ) & ( for j being Nat st j in (dom A0) \ {((len f) + 1)} & j <= 0 holds
A0 * (j,(n + 1)) = 0. F1() ) ) by A114; :: thesis: verum
end;
for k being Nat holds S3[k] from NAT_1:sch 2(A115, A34);
then consider Aa being Matrix of F2(),F3(),F1(), Bb being Matrix of F2(),F4(),F1() such that
A117: ( P1[Aa,Bb] & the_rank_of F5() = the_rank_of Aa ) and
A118: Aa * (((len f) + 1),(n + 1)) <> 0. F1() and
A119: for i, j being Nat st [i,j] in Indices Aa & i > len f & j <= n holds
Aa * (i,j) = 0. F1() and
A120: for i, j being Nat st i in dom f holds
S1[f,i,j,Aa] and
A121: for j being Nat st j in (dom Aa) \ {((len f) + 1)} & j <= F2() holds
Aa * (j,(n + 1)) = 0. F1() ;
take Aa ; :: thesis: ex B9 being Matrix of F2(),F4(),F1() st
( P1[Aa,B9] & the_rank_of F5() = the_rank_of Aa & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices Aa & i > len f & j <= n + 1 holds
Aa * (i,j) = 0. F1() ) & f is one-to-one & len f <= n + 1 & len f <= F2() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,Aa] ) ) )
take Bb ; :: thesis: ( P1[Aa,Bb] & the_rank_of F5() = the_rank_of Aa & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices Aa & i > len f & j <= n + 1 holds
Aa * (i,j) = 0. F1() ) & f is one-to-one & len f <= n + 1 & len f <= F2() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,Aa] ) ) )
thus ( P1[Aa,Bb] & the_rank_of F5() = the_rank_of Aa ) by A117; :: thesis: ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices Aa & i > len f & j <= n + 1 holds
Aa * (i,j) = 0. F1() ) & f is one-to-one & len f <= n + 1 & len f <= F2() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,Aa] ) )
take f9 = f ^ <*(n + 1)*>; :: thesis: ( ( for i, j being Nat st [i,j] in Indices Aa & i > len f9 & j <= n + 1 holds
Aa * (i,j) = 0. F1() ) & f9 is one-to-one & len f9 <= n + 1 & len f9 <= F2() & rng f9 c= Seg (n + 1) & ( for i, j being Nat st i in dom f9 holds
S1[f9,i,j,Aa] ) )
A122: len f9 = (len f) + 1 by FINSEQ_2:16;
A123: ( len Aa = F2() & dom Aa = Seg (len Aa) ) by A4, FINSEQ_1:def 3, MATRIX_0:23;
A124: now :: thesis: for i, j being Nat st [i,j] in Indices Aa & i > len f9 & j <= n + 1 holds
Aa * (i,j) = 0. F1()
let i, j be Nat; :: thesis: ( [i,j] in Indices Aa & i > len f9 & j <= n + 1 implies Aa * (b1,b2) = 0. F1() )
assume that
A125: [i,j] in Indices Aa and
A126: i > len f9 and
A127: j <= n + 1 ; :: thesis: Aa * (b1,b2) = 0. F1()
per cases ( j <= n or j = n + 1 ) by A127, NAT_1:8;
suppose A128: j <= n ; :: thesis: Aa * (b1,b2) = 0. F1()
i > len f by A122, A126, NAT_1:13;
hence Aa * (i,j) = 0. F1() by A119, A125, A128; :: thesis: verum
end;
suppose A129: j = n + 1 ; :: thesis: Aa * (b1,b2) = 0. F1()
i in dom Aa by A125, ZFMISC_1:87;
then ( i in (dom Aa) \ {((len f) + 1)} & i <= F2() ) by A122, A123, A126, FINSEQ_1:1, ZFMISC_1:56;
hence Aa * (i,j) = 0. F1() by A121, A129; :: thesis: verum
end;
end;
end;
A130: width Aa = F3() by A4, MATRIX_0:23;
A131: len f9 <= F2() by A28, A29, A122, XXREAL_0:2;
A132: now :: thesis: for i, j being Nat st i in dom f9 holds
( Aa * (i,(f9 /. i)) <> 0. F1() & ( j in dom f9 & i < j implies f9 /. i < f9 /. j ) & ( j in (dom f9) \ {i} implies Aa * (j,(f9 /. i)) = 0. F1() ) & ( j in Seg (width Aa) & j < f9 /. i implies Aa * (i,j) = 0. F1() ) )
let i, j be Nat; :: thesis: ( i in dom f9 implies ( Aa * (i,(f9 /. i)) <> 0. F1() & ( j in dom f9 & i < j implies f9 /. i < f9 /. j ) & ( j in (dom f9) \ {i} implies Aa * (j,(f9 /. i)) = 0. F1() ) & ( j in Seg (width Aa) & j < f9 /. i implies Aa * (i,j) = 0. F1() ) ) )
assume A133: i in dom f9 ; :: thesis: ( Aa * (i,(f9 /. i)) <> 0. F1() & ( j in dom f9 & i < j implies f9 /. i < f9 /. j ) & ( j in (dom f9) \ {i} implies Aa * (j,(f9 /. i)) = 0. F1() ) & ( j in Seg (width Aa) & j < f9 /. i implies Aa * (i,j) = 0. F1() ) )
A134: dom f9 = Seg ((len f) + 1) by 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
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;
now :: thesis: Aa * (i,(f9 /. i)) <> 0. F1()
per cases ( i in dom f or i in {((len f) + 1)} ) by A133, A134, XBOOLE_0:def 3;
suppose A138: i in dom f ; :: thesis: Aa * (i,(f9 /. i)) <> 0. F1()
then f /. i = f9 /. i by A135;
hence Aa * (i,(f9 /. i)) <> 0. F1() by A120, A138; :: thesis: verum
end;
suppose A139: i in {((len f) + 1)} ; :: thesis: Aa * (i,(f9 /. i)) <> 0. F1()
A140: f9 /. i = f9 . i by A133, PARTFUN1:def 6;
i = (len f) + 1 by A139, TARSKI:def 1;
hence Aa * (i,(f9 /. i)) <> 0. F1() by A118, A140, FINSEQ_1:42; :: thesis: verum
end;
end;
end;
hence Aa * (i,(f9 /. i)) <> 0. F1() ; :: thesis: ( ( j in dom f9 & i < j implies f9 /. i < f9 /. j ) & ( j in (dom f9) \ {i} implies Aa * (j,(f9 /. i)) = 0. F1() ) & ( j in Seg (width Aa) & j < f9 /. i implies Aa * (i,j) = 0. F1() ) )
thus ( j in dom f9 & i < j implies f9 /. i < f9 /. j ) :: thesis: ( ( j in (dom f9) \ {i} implies Aa * (j,(f9 /. i)) = 0. F1() ) & ( j in Seg (width Aa) & j < f9 /. i implies Aa * (i,j) = 0. F1() ) )
proof
assume that
A141: j in dom f9 and
A142: i < j ; :: thesis: f9 /. i < f9 /. j
per cases ( ( j in {((len f) + 1)} & i in {((len f) + 1)} ) or ( j in {((len f) + 1)} & i in dom f ) or ( j in dom f & i in {((len f) + 1)} ) or ( j in dom f & i in dom f ) ) by A133, A134, A141, XBOOLE_0:def 3;
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;
suppose ( j in dom f & i in {((len f) + 1)} ) ; :: thesis: f9 /. i < f9 /. j
then ( j <= len f & i = (len f) + 1 ) by A31, FINSEQ_1:1, TARSKI:def 1;
hence f9 /. i < f9 /. j by A142, NAT_1:13; :: thesis: verum
end;
suppose A147: ( j in dom f & i in dom f ) ; :: thesis: f9 /. i < f9 /. j
then ( f /. i = f9 /. i & f /. j = f9 /. j ) by A135;
hence f9 /. i < f9 /. j by A15, A142, A147; :: thesis: verum
end;
end;
end;
dom f9 = Seg (len f9) by FINSEQ_1:def 3;
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. F1() ) :: thesis: ( j in Seg (width Aa) & j < f9 /. i implies Aa * (i,j) = 0. F1() )
proof
assume A149: j in (dom f9) \ {i} ; :: thesis: Aa * (j,(f9 /. i)) = 0. F1()
per cases ( i = (len f) + 1 or i <> (len f) + 1 ) ;
suppose A150: i = (len f) + 1 ; :: thesis: Aa * (j,(f9 /. i)) = 0. F1()
(len f) + 1 in {((len f) + 1)} by TARSKI:def 1;
then (len f) + 1 in dom f9 by 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 <= F2() by A123, A148, A152, FINSEQ_1:1;
then Aa * (j,(n + 1)) = 0. F1() by A121, A150, A153;
hence Aa * (j,(f9 /. i)) = 0. F1() by A151, FINSEQ_1:42; :: thesis: verum
end;
suppose A154: i <> (len f) + 1 ; :: thesis: Aa * (j,(f9 /. i)) = 0. F1()
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 <= F3() by A7, NAT_1:13;
then f9 /. i <= F3() 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;
per cases ( j = (len f) + 1 or j <> (len f) + 1 ) ;
suppose j = (len f) + 1 ; :: thesis: Aa * (j,(f9 /. i)) = 0. F1()
then j > len f by NAT_1:13;
hence Aa * (j,(f9 /. i)) = 0. F1() by A119, A160, A161; :: thesis: verum
end;
suppose A162: j <> (len f) + 1 ; :: thesis: Aa * (j,(f9 /. i)) = 0. F1()
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. F1() by A120, A154, A156, TARSKI:def 1;
hence Aa * (j,(f9 /. i)) = 0. F1() by A135, A154, A156, TARSKI:def 1; :: thesis: verum
end;
end;
end;
end;
end;
thus ( j in Seg (width Aa) & j < f9 /. i implies Aa * (i,j) = 0. F1() ) :: thesis: verum
proof
assume that
A164: j in Seg (width Aa) and
A165: j < f9 /. i ; :: thesis: Aa * (i,j) = 0. F1()
per cases ( i in dom f or not i in dom f ) ;
suppose A166: i in dom f ; :: thesis: Aa * (i,j) = 0. F1()
then f9 /. i = f /. i by A135;
hence Aa * (i,j) = 0. F1() by A120, A164, A165, A166; :: thesis: verum
end;
end;
end;
end;
A172: ( rng <*(n + 1)*> = {(n + 1)} & (rng f) \/ {(n + 1)} c= (Seg n) \/ {(n + 1)} ) by A14, FINSEQ_1:38, XBOOLE_1:9;
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. F1() ) & f9 is one-to-one & len f9 <= n + 1 & len f9 <= F2() & rng f9 c= Seg (n + 1) & ( for i, j being Nat st i in dom f9 holds
S1[f9,i,j,Aa] ) ) by A11, A12, A28, A29, A122, A124, A172, A173, A132, FINSEQ_1:31, FINSEQ_3:91, XREAL_1:6, XXREAL_0:2; :: thesis: verum
end;
end;
end;
A174: S2[ 0 ]
proof
assume 0 <= F3() ; :: thesis: ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= 0 holds
A9 * (i,j) = 0. F1() ) & f is one-to-one & len f <= 0 & len f <= F2() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )
take A9 = F5(); :: thesis: ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= 0 holds
A9 * (i,j) = 0. F1() ) & f is one-to-one & len f <= 0 & len f <= F2() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )
take B9 = F6(); :: thesis: ( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= 0 holds
A9 * (i,j) = 0. F1() ) & f is one-to-one & len f <= 0 & len f <= F2() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )
thus ( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 ) by A1; :: thesis: ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= 0 holds
A9 * (i,j) = 0. F1() ) & f is one-to-one & len f <= 0 & len f <= F2() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) )
take f = <*> NAT; :: thesis: ( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= 0 holds
A9 * (i,j) = 0. F1() ) & f is one-to-one & len f <= 0 & len f <= F2() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) )
now :: thesis: for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= 0 holds
A9 * (i,j) = 0. F1()
let i, j be Nat; :: thesis: ( [i,j] in Indices A9 & i > len f & j <= 0 implies A9 * (i,j) = 0. F1() )
assume that
A175: [i,j] in Indices A9 and
i > len f and
A176: j <= 0 ; :: thesis: A9 * (i,j) = 0. F1()
j in Seg (width A9) by A175, ZFMISC_1:87;
hence A9 * (i,j) = 0. F1() by A176; :: thesis: verum
end;
hence ( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= 0 holds
A9 * (i,j) = 0. F1() ) & f is one-to-one & len f <= 0 & len f <= F2() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) ; :: thesis: verum
end;
for n being Nat holds S2[n] from NAT_1:sch 2(A174, A5);
then consider A9 being Matrix of F2(),F3(),F1(), B9 being Matrix of F2(),F4(),F1() such that
A177: P1[A9,B9] and
A178: the_rank_of F5() = the_rank_of A9 and
A179: ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= F3() holds
A9 * (i,j) = 0. F1() ) & f is one-to-one & len f <= F3() & len f <= F2() & rng f c= Seg F3() & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) ;
consider f being FinSequence of NAT such that
A180: for i, j being Nat st [i,j] in Indices A9 & i > len f & j <= F3() holds
A9 * (i,j) = 0. F1() and
A181: f is one-to-one and
len f <= F3() and
A182: len f <= F2() and
A183: rng f c= Seg F3() and
A184: for i, j being Nat st i in dom f holds
S1[f,i,j,A9] by A179;
A185: len A9 = F2() by A4, MATRIX_0:23;
take A9 ; :: thesis: ex B9 being Matrix of F2(),F4(),F1() st
( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ( for i being Nat st i in dom A9 & i > the_rank_of F5() holds
Line (A9,i) = F3() |-> (0. F1()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A9 & f is one-to-one & rng f c= Seg (width A9) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )
take B9 ; :: thesis: ( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 & ( for i being Nat st i in dom A9 & i > the_rank_of F5() holds
Line (A9,i) = F3() |-> (0. F1()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A9 & f is one-to-one & rng f c= Seg (width A9) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )
thus ( P1[A9,B9] & the_rank_of F5() = the_rank_of A9 ) by A177, A178; :: thesis: ( ( for i being Nat st i in dom A9 & i > the_rank_of F5() holds
Line (A9,i) = F3() |-> (0. F1()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A9 & f is one-to-one & rng f c= Seg (width A9) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) )
A186: dom A9 = Seg (len A9) by FINSEQ_1:def 3;
set L = len f;
A187: Seg (len f) c= Seg F2() by 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. F1()
proof
A190: len (diagonal_of_Matrix (Segm (A9,idL,F9))) = len f by MATRIX_3:def 10;
let k be Nat; :: thesis: ( k in dom (diagonal_of_Matrix (Segm (A9,idL,F9))) implies (diagonal_of_Matrix (Segm (A9,idL,F9))) . k <> 0. F1() )
assume k in dom (diagonal_of_Matrix (Segm (A9,idL,F9))) ; :: thesis: (diagonal_of_Matrix (Segm (A9,idL,F9))) . k <> 0. F1()
then A191: k in Seg (len f) by 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. F1() by A184, A188, A191;
hence (diagonal_of_Matrix (Segm (A9,idL,F9))) . k <> 0. F1() by A191, MATRIX_3:def 10; :: thesis: verum
end;
then A192: Product (diagonal_of_Matrix (Segm (A9,idL,F9))) <> 0. F1() by FVSUM_1:82;
now :: thesis: for i, j being Nat st [i,j] in Indices (Segm (A9,idL,F9)) & i > j holds
(Segm (A9,idL,F9)) * (i,j) = 0. F1()
let i, j be Nat; :: thesis: ( [i,j] in Indices (Segm (A9,idL,F9)) & i > j implies (Segm (A9,idL,F9)) * (i,j) = 0. F1() )
assume A193: [i,j] in Indices (Segm (A9,idL,F9)) ; :: thesis: ( i > j implies (Segm (A9,idL,F9)) * (i,j) = 0. F1() )
A194: i in Seg (len f) by A189, A193, ZFMISC_1:87;
assume i > j ; :: thesis: (Segm (A9,idL,F9)) * (i,j) = 0. F1()
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. F1() by A184, A188, A196, A195 ; :: thesis: verum
end;
then Segm (A9,idL,F9) is upper_triangular Matrix of len f,F1() by MATRIX_1:def 8;
then A197: Det (Segm (A9,idL,F9)) <> 0. F1() by 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 = F3() 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;
A201: now :: thesis: for i being Nat st i in (dom A9) \ (Seg (len f)) holds
Line (A9,i) = (width A9) |-> (0. F1())
set w0 = (width A9) |-> (0. F1());
let i be Nat; :: thesis: ( i in (dom A9) \ (Seg (len f)) implies Line (A9,i) = (width A9) |-> (0. F1()) )
assume A202: i in (dom A9) \ (Seg (len f)) ; :: thesis: Line (A9,i) = (width A9) |-> (0. F1())
set LA = Line (A9,i);
A203: now :: thesis: for j being Nat st 1 <= j & j <= width A9 holds
(Line (A9,i)) . j = ((width A9) |-> (0. F1())) . j
not i in Seg (len f) by 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. F1())) . j )
assume that
A205: 1 <= j and
A206: j <= width A9 ; :: thesis: (Line (A9,i)) . j = ((width A9) |-> (0. F1())) . j
A207: j in Seg (width A9) by 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. F1() by A180, A186, A199, A206, A208, A209, A204, FINSEQ_1:1
.= ((width A9) |-> (0. F1())) . j by A207, FINSEQ_2:57 ; :: thesis: verum
end;
( len (Line (A9,i)) = width A9 & len ((width A9) |-> (0. F1())) = width A9 ) by CARD_1:def 7;
hence Line (A9,i) = (width A9) |-> (0. F1()) by A203; :: thesis: verum
end;
then the_rank_of A9 = the_rank_of (Segm (A9,(Seg (len f)),(Seg (width A9)))) by A187, A185, A186, Th11;
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 F5() = len f by A178, A200, XXREAL_0:1;
thus for i being Nat st i in dom A9 & i > the_rank_of F5() holds
Line (A9,i) = F3() |-> (0. F1()) :: thesis: ex f being FinSequence of NAT st
( len f = the_rank_of A9 & f is one-to-one & rng f c= Seg (width A9) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) )
proof
let i be Nat; :: thesis: ( i in dom A9 & i > the_rank_of F5() implies Line (A9,i) = F3() |-> (0. F1()) )
assume that
A212: i in dom A9 and
A213: i > the_rank_of F5() ; :: thesis: Line (A9,i) = F3() |-> (0. F1())
not i in Seg (len f) by A211, A213, FINSEQ_1:1;
then i in (dom A9) \ (Seg (len f)) by A212, XBOOLE_0:def 5;
hence Line (A9,i) = F3() |-> (0. F1()) by A199, A201; :: thesis: verum
end;
take f ; :: thesis: ( len f = the_rank_of A9 & f is one-to-one & rng f c= Seg (width A9) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) )
thus ( len f = the_rank_of A9 & f is one-to-one & rng f c= Seg (width A9) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) by A4, A181, A183, A184, A200, A210, MATRIX_0:23, XXREAL_0:1; :: thesis: verum
end;
end;
end;
then consider A9 being Matrix of F2(),F3(),F1(), B9 being Matrix of F2(),F4(),F1() such that
A214: P1[A9,B9] and
A215: the_rank_of F5() = the_rank_of A9 and
A216: for i being Nat st i in dom A9 & i > the_rank_of F5() holds
Line (A9,i) = F3() |-> (0. F1()) and
A217: ex f being FinSequence of NAT st
( len f = the_rank_of A9 & f is one-to-one & rng f c= Seg (width A9) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A9] ) ) ;
consider f being FinSequence of NAT such that
A218: len f = the_rank_of A9 and
A219: f is one-to-one and
A220: rng f c= Seg (width A9) and
A221: for i, j being Nat st i in dom f holds
S1[f,i,j,A9] by A217;
not 0 in rng f by A220;
then reconsider rngf = rng f as finite without_zero Subset of NAT by A220, MEASURE6:def 2, XBOOLE_1:1;
A222: ( F2() = 0 or F2() > 0 ) ;
set S = Segm (A9,(Seg (card rngf)),rngf);
A223: dom f = Seg (the_rank_of F5()) by A215, A218, FINSEQ_1:def 3;
take A9 ; :: thesis: ex B9 being Matrix of F2(),F4(),F1() ex N being finite without_zero Subset of NAT st
( N c= Seg F3() & the_rank_of F5() = the_rank_of A9 & the_rank_of F5() = card N & P1[A9,B9] & Segm (A9,(Seg (card N)),N) is diagonal & ( for i being Nat st i in Seg (card N) holds
A9 * (i,((Sgm N) /. i)) <> 0. F1() ) & ( for i being Nat st i in dom A9 & i > card N holds
Line (A9,i) = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width A9) & j < (Sgm N) . i holds
A9 * (i,j) = 0. F1() ) )
take B9 ; :: thesis: ex N being finite without_zero Subset of NAT st
( N c= Seg F3() & the_rank_of F5() = the_rank_of A9 & the_rank_of F5() = card N & P1[A9,B9] & Segm (A9,(Seg (card N)),N) is diagonal & ( for i being Nat st i in Seg (card N) holds
A9 * (i,((Sgm N) /. i)) <> 0. F1() ) & ( for i being Nat st i in dom A9 & i > card N holds
Line (A9,i) = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width A9) & j < (Sgm N) . i holds
A9 * (i,j) = 0. F1() ) )
take rngf ; :: thesis: ( rngf c= Seg F3() & the_rank_of F5() = the_rank_of A9 & the_rank_of F5() = card rngf & P1[A9,B9] & Segm (A9,(Seg (card rngf)),rngf) is diagonal & ( for i being Nat st i in Seg (card rngf) holds
A9 * (i,((Sgm rngf) /. i)) <> 0. F1() ) & ( for i being Nat st i in dom A9 & i > card rngf holds
Line (A9,i) = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card rngf) & j in Seg (width A9) & j < (Sgm rngf) . i holds
A9 * (i,j) = 0. F1() ) )
len A9 = F2() by MATRIX_0:def 2;
then ( width A9 = 0 or width A9 = F3() ) by A222, MATRIX_0:23, MATRIX_0:def 3;
then Seg (width A9) c= Seg F3() ;
hence ( rngf c= Seg F3() & the_rank_of F5() = the_rank_of A9 ) by A215, A220; :: thesis: ( the_rank_of F5() = card rngf & P1[A9,B9] & Segm (A9,(Seg (card rngf)),rngf) is diagonal & ( for i being Nat st i in Seg (card rngf) holds
A9 * (i,((Sgm rngf) /. i)) <> 0. F1() ) & ( for i being Nat st i in dom A9 & i > card rngf holds
Line (A9,i) = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card rngf) & j in Seg (width A9) & j < (Sgm rngf) . i holds
A9 * (i,j) = 0. F1() ) )
dom f,rngf are_equipotent by A219, WELLORD2:def 4;
hence A224: card rngf = card (dom f) by CARD_1:5
.= card (Seg (the_rank_of F5())) by A215, A218, FINSEQ_1:def 3
.= the_rank_of F5() by FINSEQ_1:57 ;
:: thesis: ( P1[A9,B9] & Segm (A9,(Seg (card rngf)),rngf) is diagonal & ( for i being Nat st i in Seg (card rngf) holds
A9 * (i,((Sgm rngf) /. i)) <> 0. F1() ) & ( for i being Nat st i in dom A9 & i > card rngf holds
Line (A9,i) = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card rngf) & j in Seg (width A9) & j < (Sgm rngf) . i holds
A9 * (i,j) = 0. F1() ) )
now :: thesis: for i, j being Nat st i in dom f & j in dom f & i < j holds
f . i < f . j
let i, j be Nat; :: thesis: ( i in dom f & j in dom f & i < j implies f . i < f . j )
assume that
A225: ( i in dom f & j in dom f ) and
A226: i < j ; :: thesis: f . i < f . j
( f . i = f /. i & f . j = f /. j ) by A225, PARTFUN1:def 6;
hence f . i < f . j by A221, A225, A226; :: thesis: verum
end;
then A227: Sgm rngf = f by A219, A220, Th6;
thus P1[A9,B9] by A214; :: thesis: ( Segm (A9,(Seg (card rngf)),rngf) is diagonal & ( for i being Nat st i in Seg (card rngf) holds
A9 * (i,((Sgm rngf) /. i)) <> 0. F1() ) & ( for i being Nat st i in dom A9 & i > card rngf holds
Line (A9,i) = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card rngf) & j in Seg (width A9) & j < (Sgm rngf) . i holds
A9 * (i,j) = 0. F1() ) )
A228: card (Seg (card rngf)) = card rngf by FINSEQ_1:57;
then A229: Indices (Segm (A9,(Seg (card rngf)),rngf)) = [:(Seg (the_rank_of F5())),(Seg (the_rank_of F5())):] by A224, MATRIX_0:24;
now :: thesis: for i, j being Nat st i in Seg (the_rank_of F5()) & j in Seg (the_rank_of F5()) & i <> j holds
(Segm (A9,(Seg (card rngf)),rngf)) * (i,j) = 0. F1()
let i, j be Nat; :: thesis: ( i in Seg (the_rank_of F5()) & j in Seg (the_rank_of F5()) & i <> j implies (Segm (A9,(Seg (card rngf)),rngf)) * (i,j) = 0. F1() )
assume that
A230: i in Seg (the_rank_of F5()) and
A231: j in Seg (the_rank_of F5()) and
A232: i <> j ; :: thesis: (Segm (A9,(Seg (card rngf)),rngf)) * (i,j) = 0. F1()
A233: i in (dom f) \ {j} by A223, A230, A232, ZFMISC_1:56;
A234: (idseq (the_rank_of F5())) . 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 F5()))) . 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. F1() by A221, A223, A231, A233; :: thesis: verum
end;
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
A9 * (i,((Sgm rngf) /. i)) <> 0. F1() ) & ( for i being Nat st i in dom A9 & i > card rngf holds
Line (A9,i) = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card rngf) & j in Seg (width A9) & j < (Sgm rngf) . i holds
A9 * (i,j) = 0. F1() ) )
thus for i being Nat st i in Seg (card rngf) holds
A9 * (i,((Sgm rngf) /. i)) <> 0. F1() by A221, A224, A227, A223; :: thesis: ( ( for i being Nat st i in dom A9 & i > card rngf holds
Line (A9,i) = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card rngf) & j in Seg (width A9) & j < (Sgm rngf) . i holds
A9 * (i,j) = 0. F1() ) )
thus for i being Nat st i in dom A9 & i > card rngf holds
Line (A9,i) = F3() |-> (0. F1()) by 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. F1()
let i, j be Nat; :: thesis: ( i in Seg (card rngf) & j in Seg (width A9) & j < (Sgm rngf) . i implies A9 * (i,j) = 0. F1() )
assume that
A235: i in Seg (card rngf) and
A236: j in Seg (width A9) and
A237: j < (Sgm rngf) . i ; :: thesis: A9 * (i,j) = 0. F1()
j < f /. i by A224, A227, A223, A235, A237, PARTFUN1:def 6;
hence A9 * (i,j) = 0. F1() by A221, A224, A223, A235, A236; :: thesis: verum