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 set ONE = 1. (F1(),(card N));
A7: Indices (1. (F1(),(card N))) = [:(Seg (the_rank_of F5())),(Seg (the_rank_of F5())):] by ;
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 ;
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_0:def 2;
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 CARD_1:def 7;
( the_rank_of F5() <= len A9 & len A9 = F2() ) by ;
then A20: Seg (the_rank_of F5()) c= Seg F2() by FINSEQ_1:5;
1 <= 1 + n by NAT_1:11;
then A21: n + 1 in Seg (card N) by A10;
then A22: F2() <> 0 by ;
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_0:23;
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:19
.= ((1_ F1()) + (- (1_ F1()))) + ((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") by
.= (0. F1()) + ((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") by VECTSP_1:19
.= (A1 * ((n + 1),((Sgm N) /. (n + 1)))) " by RLVECT_1:def 4 ;
A1 * ((n + 1),((Sgm N) /. (n + 1))) <> 0. F1() by ;
hence contradiction by A26, VECTSP_1:25; :: 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 ; :: 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 ;
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:57
.= ((1_ F1()) + ((- (1_ F1())) + ((A1 * ((n + 1),((Sgm N) /. (n + 1)))) "))) * (Line (A1,(n + 1))) by FVSUM_1:55
.= (((1_ F1()) + (- (1_ F1()))) + ((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ")) * (Line (A1,(n + 1))) by RLVECT_1:def 3
.= ((0. F1()) + ((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ")) * (Line (A1,(n + 1))) by VECTSP_1:19
.= ((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") * (Line (A1,(n + 1))) by RLVECT_1:def 4 ;
A29: dom A1 = Seg (len A1) by FINSEQ_1:def 3;
A30: rng (Sgm N) = N by ;
A31: dom (Sgm N) = Seg (card N) by ;
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 ;
then A36: [i,((Sgm N) /. i)] in Indices A1 by ;
per cases ( i <= n or i = n + 1 ) by ;
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
.= 1_ F1() by ;
:: 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 ;
( (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 ;
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
.= 1_ F1() by ;
:: 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_0:26;
let i be Nat; :: according to MATRIX_1:def 6 :: 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 12;
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_0:25;
then i in Seg (card (Seg (card N))) by ;
then i in Seg (card (card N)) by FINSEQ_1:55;
then A43: ( Sgm (Seg (card N)) = idseq (card N) & (idseq (card N)) . I = I ) by ;
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 ;
( rng (Sgm (Seg (card N))) = Seg (card N) & [:(Seg (card N)),N:] c= Indices A1 ) by ;
then A45: [I,((Sgm N) . J)] in Indices A1 by ;
then A46: (Sgm N) . J in Seg (width A1) by ZFMISC_1:87;
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_0:26;
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 ;
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
.= ((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") * ((Segm (A1,(Seg (card N)),N)) * (i,j)) by
.= ((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") * (0. F1()) by A14, A41, A47, A49
.= 0. F1() ;
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
.= (Segm (A1,(Seg (card N)),N)) * (i,j) by ;
hence i = j by A14, A41, A42, A47, A44; :: 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 ;
then A51: [i,((Sgm N) /. i)] in Indices A1 by ;
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 ; :: 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 ;
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 ; :: 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 ;
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
.= 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 ;
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 ;
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
.= ((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") * (0. F1()) by A17, A27, A23, A54, A55, A56
.= 0. F1() ;
:: 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
.= 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 () & 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 () & 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 () & 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 () & 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 () & 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:57;
then A65: Indices (1. (F1(),(card N))) = Indices (Segm (A,(Seg (card N)),N)) by MATRIX_0:26;
now :: thesis: for i, j being Nat st [i,j] in Indices (1. (F1(),(card N))) holds
(Segm (A,(Seg (card N)),N)) * (i,j) = (1. (F1(),(card N))) * (i,j)
A66: dom (Sgm N) = Seg (the_rank_of F5()) by ;
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 ;
reconsider i9 = i, j9 = j as Element of NAT by ORDINAL1:def 12;
A69: i in Seg (the_rank_of F5()) by ;
then A70: (idseq (the_rank_of F5())) . i9 = i9 by FINSEQ_2:49;
A71: i <= the_rank_of F5() by ;
A72: (Segm (A,(Seg (card N)),N)) * (i,j) = A * (((Sgm (Seg (the_rank_of F5()))) . i9),((Sgm N) . j9)) by
.= A * (i9,((Sgm N) . j9)) by
.= A * (i9,((Sgm N) /. j9)) by ;
now :: thesis: (Segm (A,(Seg (card N)),N)) * (i,j) = (1. (F1(),(card N))) * (i,j)
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 ;
:: 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
.= (1. (F1(),(card N))) * (i,j) by ;
:: 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 () & j < (Sgm N) . i holds
A * (i,j) = 0. F1() ) ) by ; :: thesis: verum