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_0:24;
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_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 A5, MATRIX13:74, MATRIX_0:def 2;
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 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_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 A25, RLVECT_1:def 3
.= (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 A15, A21;
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 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_0:23;
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 FINSEQ_1:def 14;
A31: dom (Sgm N) = Seg (card N) by FINSEQ_3:40;
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 3, PARTFUN1:def 6;
then A36: [i,((Sgm N) /. i)] in Indices A1 by A4, A5, A30, A20, A29, A18, A27, A33, ZFMISC_1:87;
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_0:def 7;
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:51
.= 1_ F1() by A39, VECTSP_1:def 10 ;
:: 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 A41, ZFMISC_1:87;
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 FINSEQ_2:49, FINSEQ_3:48;
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 14, ZFMISC_1:96;
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: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 A19, A28, A45, A46, A48, MATRIX11:def 3, MATRIX_0:def 7;
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:51
.= ((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
.= 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 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; :: 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 3, PARTFUN1:def 6;
then A51: [i,((Sgm N) /. i)] in Indices A1 by A4, A5, A30, A20, A29, A18, A27, A50, ZFMISC_1:87;
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_0:def 2;
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:87;
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_0:def 7;
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:51
.= ((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 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: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 A5, FINSEQ_3:40;
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:87;
reconsider i9 = i, j9 = j as Element of NAT by ORDINAL1:def 12;
A69: i in Seg (the_rank_of F5()) by A7, A67, ZFMISC_1:87;
then A70: (idseq (the_rank_of F5())) . i9 = i9 by FINSEQ_2:49;
A71: i <= the_rank_of F5() by A69, FINSEQ_1:1;
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:48
.= A * (i9,((Sgm N) /. j9)) by A68, A66, PARTFUN1:def 6 ;
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 A67, A73, MATRIX_1:def 3 ;
:: 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
.= (1. (F1(),(card N))) * (i,j) by A67, A74, MATRIX_1:def 3 ;
:: 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_0:27; :: thesis: verum