set r = the_rank_of F5();
A3: for A9 being Matrix of F2(),F3(),F1()
for B9 being Matrix of F2(),F4(),F1() st P1[A9,B9] holds
for i, j being Nat st i <> j & j in dom A9 holds
for a being Element of F1() holds P1[ RLine A9,i,((Line A9,i) + (a * (Line A9,j))),F7(B9,i,j,a)] by A2;
consider A9 being Matrix of F2(),F3(),F1(), B9 being Matrix of F2(),F4(),F1(), N being finite without_zero Subset of NAT such that
A4: N c= Seg F3() and
A5: ( the_rank_of F5() = the_rank_of A9 & the_rank_of F5() = card N ) and
A6: ( 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() ) ) from MATRIX15:sch 1(A1, A3);
 set ONE = 1. F1(),(card N);
A7: Indices (1. F1(),(card N)) = [:(Seg (the_rank_of F5())),(Seg (the_rank_of F5())):] by A5, MATRIX_1:25;
defpred S1[ Nat] means ( $1 <= card N implies ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( the_rank_of F5() = the_rank_of A9 & ( for i being Nat st i in Seg (card N) & i <= $1 holds
A9 * i,((Sgm N) /. i) = 1_ F1() ) & 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() ) ) );
A8: for n being Nat st S1[n] holds
S1[n + 1]
proof
set f = Sgm N;
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A9: S1[n] ; :: thesis: S1[n + 1]
set n1 = n + 1;
assume A10: n + 1 <= card N ; :: thesis: ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() st
( the_rank_of F5() = the_rank_of A9 & ( for i being Nat st i in Seg (card N) & i <= n + 1 holds
A9 * i,((Sgm N) /. i) = 1_ F1() ) & 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() ) )
then consider A1 being Matrix of F2(),F3(),F1(), A25 being Matrix of F2(),F4(),F1() such that
A11: the_rank_of F5() = the_rank_of A1 and
A12: for i being Nat st i in Seg (card N) & i <= n holds
A1 * i,((Sgm N) /. i) = 1_ F1() and
A13: P1[A1,A25] and
A14: Segm A1,(Seg (card N)),N is diagonal and
A15: for i being Nat st i in Seg (card N) holds
A1 * i,((Sgm N) /. i) <> 0. F1() and
A16: for i being Nat st i in dom A1 & i > card N holds
Line A1,i = F3() |-> (0. F1()) and
A17: for i, j being Nat st i in Seg (card N) & j in Seg (width A1) & j < (Sgm N) . i holds
A1 * i,j = 0. F1() by A9, NAT_1:13;
set L = Line A1,(n + 1);
set LL = (Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1)));
set R = RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))));
take RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1)))) ; :: thesis: ex B9 being Matrix of F2(),F4(),F1() st
( the_rank_of F5() = the_rank_of (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) & ( for i being Nat st i in Seg (card N) & i <= n + 1 holds
(RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,((Sgm N) /. i) = 1_ F1() ) & P1[ RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1)))),B9] & Segm (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),(Seg (card N)),N is diagonal & ( for i being Nat st i in Seg (card N) holds
(RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,((Sgm N) /. i) <> 0. F1() ) & ( for i being Nat st i in dom (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) & i > card N holds
Line (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),i = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1)))))) & j < (Sgm N) . i holds
(RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,j = 0. F1() ) )
take FB = F7(A25,(n + 1),(n + 1),(((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1()))); :: thesis: ( the_rank_of F5() = the_rank_of (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) & ( for i being Nat st i in Seg (card N) & i <= n + 1 holds
(RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,((Sgm N) /. i) = 1_ F1() ) & P1[ RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1)))),FB] & Segm (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),(Seg (card N)),N is diagonal & ( for i being Nat st i in Seg (card N) holds
(RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,((Sgm N) /. i) <> 0. F1() ) & ( for i being Nat st i in dom (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) & i > card N holds
Line (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),i = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1)))))) & j < (Sgm N) . i holds
(RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,j = 0. F1() ) )
A18: len A1 = F2() by MATRIX_1:def 3;
set SA = Segm A1,(Seg (card N)),N;
set S = Segm (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),(Seg (card N)),N;
A19: len ((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1)))) = width A1 by FINSEQ_1:def 18;
( the_rank_of F5() <= len A9 & len A9 = F2() ) by A5, MATRIX13:74, MATRIX_1:def 3;
then A20: Seg (the_rank_of F5()) c= Seg F2() by FINSEQ_1:7;
1 <= 1 + n by NAT_1:11;
then A21: n + 1 in Seg (card N) by A10;
then A22: F2() <> 0 by A5, A20;
then A23: width (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) = F3() by MATRIX_1:24;
A24: ((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1()) <> - (1. F1())
proof
assume A25: ((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1()) = - (1. F1()) ; :: thesis: contradiction
A26: 0. F1() = (1_ F1()) + (- (1_ F1())) by VECTSP_1:66
.= ((1_ F1()) + (- (1_ F1()))) + ((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) by A25, RLVECT_1:def 6
.= (0. F1()) + ((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) by VECTSP_1:66
.= (A1 * (n + 1),((Sgm N) /. (n + 1))) " by RLVECT_1:def 7 ;
A1 * (n + 1),((Sgm N) /. (n + 1)) <> 0. F1() by A15, A21;
hence contradiction by A26, VECTSP_1:74; :: thesis: verum
end;
hence the_rank_of (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) = the_rank_of F5() by A5, A11, A21, A20, A18, MATRIX13:92; :: thesis: ( ( for i being Nat st i in Seg (card N) & i <= n + 1 holds
(RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,((Sgm N) /. i) = 1_ F1() ) & P1[ RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1)))),FB] & Segm (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),(Seg (card N)),N is diagonal & ( for i being Nat st i in Seg (card N) holds
(RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,((Sgm N) /. i) <> 0. F1() ) & ( for i being Nat st i in dom (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) & i > card N holds
Line (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),i = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1)))))) & j < (Sgm N) . i holds
(RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,j = 0. F1() ) )
A27: width A1 = F3() by A22, MATRIX_1:24;
A28: (Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))) = ((1_ F1()) * (Line A1,(n + 1))) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))) by FVSUM_1:70
.= ((1_ F1()) + ((- (1_ F1())) + ((A1 * (n + 1),((Sgm N) /. (n + 1))) " ))) * (Line A1,(n + 1)) by FVSUM_1:68
.= (((1_ F1()) + (- (1_ F1()))) + ((A1 * (n + 1),((Sgm N) /. (n + 1))) " )) * (Line A1,(n + 1)) by RLVECT_1:def 6
.= ((0. F1()) + ((A1 * (n + 1),((Sgm N) /. (n + 1))) " )) * (Line A1,(n + 1)) by VECTSP_1:66
.= ((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) * (Line A1,(n + 1)) by RLVECT_1:def 7 ;
A29: dom A1 = Seg (len A1) by FINSEQ_1:def 3;
A30: rng (Sgm N) = N by A4, FINSEQ_1:def 13;
A31: dom (Sgm N) = Seg (card N) by A4, FINSEQ_3:45;
thus A32: for i being Nat st i in Seg (card N) & i <= n + 1 holds
(RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,((Sgm N) /. i) = 1_ F1() :: thesis: ( P1[ RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1)))),FB] & Segm (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),(Seg (card N)),N is diagonal & ( for i being Nat st i in Seg (card N) holds
(RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,((Sgm N) /. i) <> 0. F1() ) & ( for i being Nat st i in dom (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) & i > card N holds
Line (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),i = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1)))))) & j < (Sgm N) . i holds
(RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,j = 0. F1() ) )
proof
let i be Nat; :: thesis: ( i in Seg (card N) & i <= n + 1 implies (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,((Sgm N) /. i) = 1_ F1() )
assume that
A33: i in Seg (card N) and
A34: i <= n + 1 ; :: thesis: (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,((Sgm N) /. i) = 1_ F1()
A35: ( (Sgm N) . i = (Sgm N) /. i & (Sgm N) . i in rng (Sgm N) ) by A31, A33, FUNCT_1:def 5, PARTFUN1:def 8;
then A36: [i,((Sgm N) /. i)] in Indices A1 by A4, A5, A30, A20, A29, A18, A27, A33, ZFMISC_1:106;
per cases ( i <= n or i = n + 1 ) by A34, NAT_1:8;
suppose A37: i <= n ; :: thesis: (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,((Sgm N) /. i) = 1_ F1()
then i < n + 1 by NAT_1:13;
hence (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,((Sgm N) /. i) = A1 * i,((Sgm N) /. i) by A19, A36, MATRIX11:def 3
.= 1_ F1() by A12, A33, A37 ;
:: thesis: verum
end;
suppose A38: i = n + 1 ; :: thesis: (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,((Sgm N) /. i) = 1_ F1()
A39: A1 * i,((Sgm N) /. i) <> 0. F1() by A15, A33;
( (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,((Sgm N) /. i) = (((A1 * i,((Sgm N) /. i)) " ) * (Line A1,(n + 1))) . ((Sgm N) /. i) & (Line A1,(n + 1)) . ((Sgm N) /. i) = A1 * i,((Sgm N) /. i) ) by A4, A30, A19, A28, A27, A35, A36, A38, MATRIX11:def 3, MATRIX_1:def 8;
hence (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,((Sgm N) /. i) = ((A1 * i,((Sgm N) /. i)) " ) * (A1 * i,((Sgm N) /. i)) by A4, A30, A27, A35, FVSUM_1:63
.= 1_ F1() by A39, VECTSP_1:def 22 ;
:: thesis: verum
end;
end;
end;
thus P1[ RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1)))),FB] by A2, A5, A13, A21, A20, A29, A18, A24; :: thesis: ( Segm (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),(Seg (card N)),N is diagonal & ( for i being Nat st i in Seg (card N) holds
(RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,((Sgm N) /. i) <> 0. F1() ) & ( for i being Nat st i in dom (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) & i > card N holds
Line (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),i = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1)))))) & j < (Sgm N) . i holds
(RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,j = 0. F1() ) )
thus Segm (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),(Seg (card N)),N is diagonal :: thesis: ( ( for i being Nat st i in Seg (card N) holds
(RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,((Sgm N) /. i) <> 0. F1() ) & ( for i being Nat st i in dom (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) & i > card N holds
Line (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),i = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1)))))) & j < (Sgm N) . i holds
(RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,j = 0. F1() ) )
proof
A40: Indices A1 = Indices (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) by MATRIX_1:27;
let i be Nat; :: according to MATRIX_1:def 15 :: thesis: for b1 being set holds
( not [i,b1] in Indices (Segm (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),(Seg (card N)),N) or (Segm (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),(Seg (card N)),N) * i,b1 = 0. F1() or i = b1 )
let j be Nat; :: thesis: ( not [i,j] in Indices (Segm (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),(Seg (card N)),N) or (Segm (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),(Seg (card N)),N) * i,j = 0. F1() or i = j )
assume that
A41: [i,j] in Indices (Segm (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),(Seg (card N)),N) and
A42: (Segm (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),(Seg (card N)),N) * i,j <> 0. F1() ; :: thesis: i = j
reconsider I = i, J = j as Element of NAT by ORDINAL1:def 13;
Indices (Segm (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),(Seg (card N)),N) = [:(Seg (card (Seg (card N)))),(Seg (width (Segm (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),(Seg (card N)),N))):] by MATRIX_1:26;
then i in Seg (card (Seg (card N))) by A41, ZFMISC_1:106;
then i in Seg (card (card N)) by FINSEQ_1:76;
then A43: ( Sgm (Seg (card N)) = idseq (card N) & (idseq (card N)) . I = I ) by FINSEQ_2:57, FINSEQ_3:54;
then A44: (Segm (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),(Seg (card N)),N) * i,j = (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * I,((Sgm N) . J) by A41, MATRIX13:def 1;
( rng (Sgm (Seg (card N))) = Seg (card N) & [:(Seg (card N)),N:] c= Indices A1 ) by A4, A5, A20, A29, A18, A27, FINSEQ_1:def 13, ZFMISC_1:119;
then A45: [I,((Sgm N) . J)] in Indices A1 by A30, A41, A40, A43, MATRIX13:17;
then A46: (Sgm N) . J in Seg (width A1) by ZFMISC_1:106;
then reconsider SgmNJ = (Sgm N) . j as Element of NAT ;
A47: Indices (Segm (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),(Seg (card N)),N) = Indices (Segm A1,(Seg (card N)),N) by MATRIX_1:27;
per cases ( I = n + 1 or I <> n + 1 ) ;
suppose A48: I = n + 1 ; :: thesis: i = j
thus i = j :: thesis: verum
proof
assume A49: i <> j ; :: thesis: contradiction
( (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * I,((Sgm N) . J) = (((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) * (Line A1,(n + 1))) . SgmNJ & (Line A1,(n + 1)) . SgmNJ = A1 * I,SgmNJ ) by A19, A28, A45, A46, A48, MATRIX11:def 3, MATRIX_1:def 8;
then (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * I,((Sgm N) . J) = ((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) * (A1 * I,SgmNJ) by A46, FVSUM_1:63
.= ((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) * ((Segm A1,(Seg (card N)),N) * i,j) by A41, A47, A43, MATRIX13:def 1
.= ((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) * (0. F1()) by A14, A41, A47, A49, MATRIX_1:def 15
.= 0. F1() by VECTSP_1:36 ;
hence contradiction by A41, A42, A43, MATRIX13:def 1; :: thesis: verum
end;
end;
suppose I <> n + 1 ; :: thesis: i = j
then (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * I,((Sgm N) . J) = A1 * ((Sgm (Seg (card N))) . I),((Sgm N) . J) by A19, A43, A45, MATRIX11:def 3
.= (Segm A1,(Seg (card N)),N) * i,j by A41, A47, MATRIX13:def 1 ;
hence i = j by A14, A41, A42, A47, A44, MATRIX_1:def 15; :: thesis: verum
end;
end;
end;
thus for i being Nat st i in Seg (card N) holds
(RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,((Sgm N) /. i) <> 0. F1() :: thesis: ( ( for i being Nat st i in dom (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) & i > card N holds
Line (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),i = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1)))))) & j < (Sgm N) . i holds
(RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,j = 0. F1() ) )
proof
let i be Nat; :: thesis: ( i in Seg (card N) implies (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,((Sgm N) /. i) <> 0. F1() )
assume A50: i in Seg (card N) ; :: thesis: (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,((Sgm N) /. i) <> 0. F1()
( (Sgm N) . i = (Sgm N) /. i & (Sgm N) . i in rng (Sgm N) ) by A31, A50, FUNCT_1:def 5, PARTFUN1:def 8;
then A51: [i,((Sgm N) /. i)] in Indices A1 by A4, A5, A30, A20, A29, A18, A27, A50, ZFMISC_1:106;
per cases ( i = n + 1 or i <> n + 1 ) ;
suppose i = n + 1 ; :: thesis: (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,((Sgm N) /. i) <> 0. F1()
hence (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,((Sgm N) /. i) <> 0. F1() by A32, A50; :: thesis: verum
end;
suppose i <> n + 1 ; :: thesis: (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,((Sgm N) /. i) <> 0. F1()
then (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,((Sgm N) /. i) = A1 * i,((Sgm N) /. i) by A19, A51, MATRIX11:def 3;
hence (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,((Sgm N) /. i) <> 0. F1() by A15, A50; :: thesis: verum
end;
end;
end;
thus for i being Nat st i in dom (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) & i > card N holds
Line (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),i = F3() |-> (0. F1()) :: thesis: for i, j being Nat st i in Seg (card N) & j in Seg (width (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1)))))) & j < (Sgm N) . i holds
(RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,j = 0. F1()
proof
A52: ( dom (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) = Seg (len (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1)))))) & len (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) = F2() ) by FINSEQ_1:def 3, MATRIX_1:def 3;
let i be Nat; :: thesis: ( i in dom (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) & i > card N implies Line (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),i = F3() |-> (0. F1()) )
assume A53: ( i in dom (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) & i > card N ) ; :: thesis: Line (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),i = F3() |-> (0. F1())
thus Line (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))),i = Line A1,i by A10, A53, A52, MATRIX11:28
.= F3() |-> (0. F1()) by A16, A29, A18, A53, A52 ; :: thesis: verum
end;
let i, j be Nat; :: thesis: ( i in Seg (card N) & j in Seg (width (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1)))))) & j < (Sgm N) . i implies (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,j = 0. F1() )
assume that
A54: i in Seg (card N) and
A55: j in Seg (width (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1)))))) and
A56: j < (Sgm N) . i ; :: thesis: (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,j = 0. F1()
A57: [i,j] in Indices A1 by A5, A20, A29, A18, A27, A23, A54, A55, ZFMISC_1:106;
per cases ( i = n + 1 or i <> n + 1 ) ;
suppose i = n + 1 ; :: thesis: (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,j = 0. F1()
then ( (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,j = (((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) * (Line A1,(n + 1))) . j & (Line A1,(n + 1)) . j = A1 * i,j ) by A19, A28, A27, A23, A55, A57, MATRIX11:def 3, MATRIX_1:def 8;
hence (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,j = ((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) * (A1 * i,j) by A27, A23, A55, FVSUM_1:63
.= ((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) * (0. F1()) by A17, A27, A23, A54, A55, A56
.= 0. F1() by VECTSP_1:36 ;
:: thesis: verum
end;
suppose i <> n + 1 ; :: thesis: (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,j = 0. F1()
hence (RLine A1,(n + 1),((Line A1,(n + 1)) + ((((A1 * (n + 1),((Sgm N) /. (n + 1))) " ) - (1_ F1())) * (Line A1,(n + 1))))) * i,j = A1 * i,j by A19, A57, MATRIX11:def 3
.= 0. F1() by A17, A27, A23, A54, A55, A56 ;
:: thesis: verum
end;
end;
end;
for i being Nat st i in Seg (card N) & i <= 0 holds
A9 * i,((Sgm N) /. i) = 1_ F1() ;
then A58: S1[ 0 ] by A5, A6;
for n being Nat holds S1[n] from NAT_1:sch 2(A58, A8);
 then consider A being Matrix of F2(),F3(),F1(), B being Matrix of F2(),F4(),F1() such that
A59: the_rank_of F5() = the_rank_of A and
A60: for i being Nat st i in Seg (card N) & i <= card N holds
A * i,((Sgm N) /. i) = 1_ F1() and
A61: P1[A,B] and
A62: Segm A,(Seg (card N)),N is diagonal and
for i being Nat st i in Seg (card N) holds
A * i,((Sgm N) /. i) <> 0. F1() and
A63: ( ( for i being Nat st i in dom A & i > card N holds
Line A,i = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width A) & j < (Sgm N) . i holds
A * i,j = 0. F1() ) ) ;
take A ; :: 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 A & the_rank_of F5() = card N & P1[A,B9] & Segm A,(Seg (card N)),N = 1. F1(),(card N) & ( for i being Nat st i in dom A & i > card N holds
Line A,i = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width A) & j < (Sgm N) . i holds
A * i,j = 0. F1() ) )
take B ; :: thesis: ex N being finite without_zero Subset of NAT st
( N c= Seg F3() & the_rank_of F5() = the_rank_of A & the_rank_of F5() = card N & P1[A,B] & Segm A,(Seg (card N)),N = 1. F1(),(card N) & ( for i being Nat st i in dom A & i > card N holds
Line A,i = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width A) & j < (Sgm N) . i holds
A * i,j = 0. F1() ) )
take N ; :: thesis: ( N c= Seg F3() & the_rank_of F5() = the_rank_of A & the_rank_of F5() = card N & P1[A,B] & Segm A,(Seg (card N)),N = 1. F1(),(card N) & ( for i being Nat st i in dom A & i > card N holds
Line A,i = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width A) & j < (Sgm N) . i holds
A * i,j = 0. F1() ) )
thus ( N c= Seg F3() & the_rank_of F5() = the_rank_of A & the_rank_of F5() = card N & P1[A,B] ) by A4, A5, A59, A61; :: thesis: ( Segm A,(Seg (card N)),N = 1. F1(),(card N) & ( for i being Nat st i in dom A & i > card N holds
Line A,i = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width A) & j < (Sgm N) . i holds
A * i,j = 0. F1() ) )
set S = Segm A,(Seg (card N)),N;
A64: card (Seg (card N)) = card N by FINSEQ_1:78;
then A65: Indices (1. F1(),(card N)) = Indices (Segm A,(Seg (card N)),N) by MATRIX_1:27;
now
A66: dom (Sgm N) = Seg (the_rank_of F5()) by A4, A5, FINSEQ_3:45;
let i, j be Nat; :: thesis: ( [i,j] in Indices (1. F1(),(card N)) implies (Segm A,(Seg (card N)),N) * i,j = (1. F1(),(card N)) * i,j )
assume A67: [i,j] in Indices (1. F1(),(card N)) ; :: thesis: (Segm A,(Seg (card N)),N) * i,j = (1. F1(),(card N)) * i,j
A68: j in Seg (the_rank_of F5()) by A7, A67, ZFMISC_1:106;
reconsider i9 = i, j9 = j as Element of NAT by ORDINAL1:def 13;
A69: i in Seg (the_rank_of F5()) by A7, A67, ZFMISC_1:106;
then A70: (idseq (the_rank_of F5())) . i9 = i9 by FINSEQ_2:57;
A71: i <= the_rank_of F5() by A69, FINSEQ_1:3;
A72: (Segm A,(Seg (card N)),N) * i,j = A * ((Sgm (Seg (the_rank_of F5()))) . i9),((Sgm N) . j9) by A5, A65, A67, MATRIX13:def 1
.= A * i9,((Sgm N) . j9) by A70, FINSEQ_3:54
.= A * i9,((Sgm N) /. j9) by A68, A66, PARTFUN1:def 8 ;
now
per cases ( i9 = j9 or i9 <> j9 ) ;
suppose A73: i9 = j9 ; :: thesis: (Segm A,(Seg (card N)),N) * i,j = (1. F1(),(card N)) * i,j
hence (Segm A,(Seg (card N)),N) * i,j = 1_ F1() by A5, A60, A69, A71, A72
.= (1. F1(),(card N)) * i,j by A67, A73, MATRIX_1:def 12 ;
:: thesis: verum
end;
suppose A74: i9 <> j9 ; :: thesis: (Segm A,(Seg (card N)),N) * i,j = (1. F1(),(card N)) * i,j
hence (Segm A,(Seg (card N)),N) * i,j = 0. F1() by A62, A65, A67, MATRIX_1:def 15
.= (1. F1(),(card N)) * i,j by A67, A74, MATRIX_1:def 12 ;
:: thesis: verum
end;
end;
end;
hence (Segm A,(Seg (card N)),N) * i,j = (1. F1(),(card N)) * i,j ; :: thesis: verum
end;
hence ( Segm A,(Seg (card N)),N = 1. F1(),(card N) & ( for i being Nat st i in dom A & i > card N holds
Line A,i = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width A) & j < (Sgm N) . i holds
A * i,j = 0. F1() ) ) by A63, A64, MATRIX_1:28; :: thesis: verum