set r = the_rank_of F_{5}();

A3: for A9 being Matrix of F_{2}(),F_{3}(),F_{1}()

for B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st P_{1}[A9,B9] holds

for i, j being Nat st i <> j & j in dom A9 holds

for a being Element of F_{1}() holds P_{1}[ RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))),F_{7}(B9,i,j,a)]
by A2;

consider A9 being Matrix of F_{2}(),F_{3}(),F_{1}(), B9 being Matrix of F_{2}(),F_{4}(),F_{1}(), N being finite without_zero Subset of NAT such that

A4: N c= Seg F_{3}()
and

A5: ( the_rank_of F_{5}() = the_rank_of A9 & the_rank_of F_{5}() = card N )
and

A6: ( P_{1}[A9,B9] & Segm (A9,(Seg (card N)),N) is diagonal & ( for i being Nat st i in Seg (card N) holds

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

Line (A9,i) = F_{3}() |-> (0. F_{1}()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width A9) & j < (Sgm N) . i holds

A9 * (i,j) = 0. F_{1}() ) )
from MATRIX15:sch 1(A1, A3);

set ONE = 1. (F_{1}(),(card N));

A7: Indices (1. (F_{1}(),(card N))) = [:(Seg (the_rank_of F_{5}())),(Seg (the_rank_of F_{5}())):]
by A5, MATRIX_0:24;

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

( the_rank_of F_{5}() = the_rank_of A9 & ( for i being Nat st i in Seg (card N) & i <= $1 holds

A9 * (i,((Sgm N) /. i)) = 1_ F_{1}() ) & P_{1}[A9,B9] & Segm (A9,(Seg (card N)),N) is diagonal & ( for i being Nat st i in Seg (card N) holds

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

Line (A9,i) = F_{3}() |-> (0. F_{1}()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width A9) & j < (Sgm N) . i holds

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

A8: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

A9 * (i,((Sgm N) /. i)) = 1_ F_{1}()
;

then A58: S_{1}[ 0 ]
by A5, A6;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A58, A8);

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

A59: the_rank_of F_{5}() = 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_ F_{1}()
and

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

A63: ( ( for i being Nat st i in dom A & i > card N holds

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

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

( N c= Seg F_{3}() & the_rank_of F_{5}() = the_rank_of A & the_rank_of F_{5}() = card N & P_{1}[A,B9] & Segm (A,(Seg (card N)),N) = 1. (F_{1}(),(card N)) & ( for i being Nat st i in dom A & i > card N holds

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

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

( N c= Seg F_{3}() & the_rank_of F_{5}() = the_rank_of A & the_rank_of F_{5}() = card N & P_{1}[A,B] & Segm (A,(Seg (card N)),N) = 1. (F_{1}(),(card N)) & ( for i being Nat st i in dom A & i > card N holds

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

take N ; :: thesis: ( N c= Seg F_{3}() & the_rank_of F_{5}() = the_rank_of A & the_rank_of F_{5}() = card N & P_{1}[A,B] & Segm (A,(Seg (card N)),N) = 1. (F_{1}(),(card N)) & ( for i being Nat st i in dom A & i > card N holds

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

thus ( N c= Seg F_{3}() & the_rank_of F_{5}() = the_rank_of A & the_rank_of F_{5}() = card N & P_{1}[A,B] )
by A4, A5, A59, A61; :: thesis: ( Segm (A,(Seg (card N)),N) = 1. (F_{1}(),(card N)) & ( for i being Nat st i in dom A & i > card N holds

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

set S = Segm (A,(Seg (card N)),N);

A64: card (Seg (card N)) = card N by FINSEQ_1:57;

then A65: Indices (1. (F_{1}(),(card N))) = Indices (Segm (A,(Seg (card N)),N))
by MATRIX_0:26;

_{1}(),(card N)) & ( for i being Nat st i in dom A & i > card N holds

Line (A,i) = F_{3}() |-> (0. F_{1}()) ) & ( 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. F_{1}() ) )
by A63, A64, MATRIX_0:27; :: thesis: verum

A3: for A9 being Matrix of F

for B9 being Matrix of F

for i, j being Nat st i <> j & j in dom A9 holds

for a being Element of F

consider A9 being Matrix of F

A4: N c= Seg F

A5: ( the_rank_of F

A6: ( P

A9 * (i,((Sgm N) /. i)) <> 0. F

Line (A9,i) = F

A9 * (i,j) = 0. F

set ONE = 1. (F

A7: Indices (1. (F

defpred S

( the_rank_of F

A9 * (i,((Sgm N) /. i)) = 1_ F

A9 * (i,((Sgm N) /. i)) <> 0. F

Line (A9,i) = F

A9 * (i,j) = 0. F

A8: for n being Nat st S

S

proof

for i being Nat st i in Seg (card N) & i <= 0 holds
set f = Sgm N;

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

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

set n1 = n + 1;

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

( the_rank_of F_{5}() = the_rank_of A9 & ( for i being Nat st i in Seg (card N) & i <= n + 1 holds

A9 * (i,((Sgm N) /. i)) = 1_ F_{1}() ) & P_{1}[A9,B9] & Segm (A9,(Seg (card N)),N) is diagonal & ( for i being Nat st i in Seg (card N) holds

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

Line (A9,i) = F_{3}() |-> (0. F_{1}()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width A9) & j < (Sgm N) . i holds

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

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

A11: the_rank_of F_{5}() = 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_ F_{1}()
and

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

A16: for i being Nat st i in dom A1 & i > card N holds

Line (A1,i) = F_{3}() |-> (0. F_{1}())
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. F_{1}()
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_ F_{1}())) * (Line (A1,(n + 1))));

set R = RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (Line (A1,(n + 1))))));

take RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (Line (A1,(n + 1))))))
; :: thesis: ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st

( the_rank_of F_{5}() = the_rank_of (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,((Sgm N) /. i)) = 1_ F_{1}() ) & P_{1}[ RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (Line (A1,(n + 1)))))),B9] & Segm ((RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,((Sgm N) /. i)) <> 0. F_{1}() ) & ( for i being Nat st i in dom (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))),i) = F_{3}() |-> (0. F_{1}()) ) & ( 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_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,j) = 0. F_{1}() ) )

take FB = F_{7}(A25,(n + 1),(n + 1),(((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}()))); :: thesis: ( the_rank_of F_{5}() = the_rank_of (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,((Sgm N) /. i)) = 1_ F_{1}() ) & P_{1}[ RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (Line (A1,(n + 1)))))),FB] & Segm ((RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,((Sgm N) /. i)) <> 0. F_{1}() ) & ( for i being Nat st i in dom (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))),i) = F_{3}() |-> (0. F_{1}()) ) & ( 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_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,j) = 0. F_{1}() ) )

A18: len A1 = F_{2}()
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_ F_{1}())) * (Line (A1,(n + 1))))))),(Seg (card N)),N);

A19: len ((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (Line (A1,(n + 1))))) = width A1
by CARD_1:def 7;

( the_rank_of F_{5}() <= len A9 & len A9 = F_{2}() )
by A5, MATRIX13:74, MATRIX_0:def 2;

then A20: Seg (the_rank_of F_{5}()) c= Seg F_{2}()
by FINSEQ_1:5;

1 <= 1 + n by NAT_1:11;

then A21: n + 1 in Seg (card N) by A10;

then A22: F_{2}() <> 0
by A5, A20;

then A23: width (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (Line (A1,(n + 1))))))) = F_{3}()
by MATRIX_0:23;

A24: ((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}()) <> - (1. F_{1}())
_{1}())) * (Line (A1,(n + 1))))))) = the_rank_of F_{5}()
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_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,((Sgm N) /. i)) = 1_ F_{1}() ) & P_{1}[ RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (Line (A1,(n + 1)))))),FB] & Segm ((RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,((Sgm N) /. i)) <> 0. F_{1}() ) & ( for i being Nat st i in dom (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))),i) = F_{3}() |-> (0. F_{1}()) ) & ( 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_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,j) = 0. F_{1}() ) )

A27: width A1 = F_{3}()
by A22, MATRIX_0:23;

A28: (Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (Line (A1,(n + 1)))) =
((1_ F_{1}()) * (Line (A1,(n + 1)))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (Line (A1,(n + 1))))
by FVSUM_1:57

.= ((1_ F_{1}()) + ((- (1_ F_{1}())) + ((A1 * ((n + 1),((Sgm N) /. (n + 1)))) "))) * (Line (A1,(n + 1)))
by FVSUM_1:55

.= (((1_ F_{1}()) + (- (1_ F_{1}()))) + ((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ")) * (Line (A1,(n + 1)))
by RLVECT_1:def 3

.= ((0. F_{1}()) + ((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 A4, FINSEQ_1:def 13;

A31: dom (Sgm N) = Seg (card N) by A4, 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_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,((Sgm N) /. i)) = 1_ F_{1}()
:: thesis: ( P_{1}[ RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (Line (A1,(n + 1)))))),FB] & Segm ((RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,((Sgm N) /. i)) <> 0. F_{1}() ) & ( for i being Nat st i in dom (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))),i) = F_{3}() |-> (0. F_{1}()) ) & ( 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_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,j) = 0. F_{1}() ) )_{1}[ RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (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_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,((Sgm N) /. i)) <> 0. F_{1}() ) & ( for i being Nat st i in dom (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))),i) = F_{3}() |-> (0. F_{1}()) ) & ( 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_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,j) = 0. F_{1}() ) )

thus Segm ((RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,((Sgm N) /. i)) <> 0. F_{1}() ) & ( for i being Nat st i in dom (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))),i) = F_{3}() |-> (0. F_{1}()) ) & ( 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_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,j) = 0. F_{1}() ) )

(RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,((Sgm N) /. i)) <> 0. F_{1}()
:: 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_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))),i) = F_{3}() |-> (0. F_{1}()) ) & ( 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_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,j) = 0. F_{1}() ) )_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))),i) = F_{3}() |-> (0. F_{1}())
:: 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_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,j) = 0. F_{1}()_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,j) = 0. F_{1}() )

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_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,j) = 0. F_{1}()

A57: [i,j] in Indices A1 by A5, A20, A29, A18, A27, A23, A54, A55, ZFMISC_1:87;

end;let n be Nat; :: thesis: ( S

assume A9: S

set n1 = n + 1;

assume A10: n + 1 <= card N ; :: thesis: ex A9 being Matrix of F

( the_rank_of F

A9 * (i,((Sgm N) /. i)) = 1_ F

A9 * (i,((Sgm N) /. i)) <> 0. F

Line (A9,i) = F

A9 * (i,j) = 0. F

then consider A1 being Matrix of F

A11: the_rank_of F

A12: for i being Nat st i in Seg (card N) & i <= n holds

A1 * (i,((Sgm N) /. i)) = 1_ F

A13: P

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

A16: for i being Nat st i in dom A1 & i > card N holds

Line (A1,i) = F

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

set L = Line (A1,(n + 1));

set LL = (Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

set R = RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

take RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

( the_rank_of F

(RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

(RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

Line ((RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

(RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

take FB = F

(RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

(RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

Line ((RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

(RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

A18: len A1 = F

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

A19: len ((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

( the_rank_of F

then A20: Seg (the_rank_of F

1 <= 1 + n by NAT_1:11;

then A21: n + 1 in Seg (card N) by A10;

then A22: F

then A23: width (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

A24: ((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

proof

hence
the_rank_of (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F
assume A25:
((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}()) = - (1. F_{1}())
; :: thesis: contradiction

A26: 0. F_{1}() =
(1_ F_{1}()) + (- (1_ F_{1}()))
by VECTSP_1:19

.= ((1_ F_{1}()) + (- (1_ F_{1}()))) + ((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ")
by A25, RLVECT_1:def 3

.= (0. F_{1}()) + ((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. F_{1}()
by A15, A21;

hence contradiction by A26, VECTSP_1:25; :: thesis: verum

end;A26: 0. F

.= ((1_ F

.= (0. F

.= (A1 * ((n + 1),((Sgm N) /. (n + 1)))) " by RLVECT_1:def 4 ;

A1 * ((n + 1),((Sgm N) /. (n + 1))) <> 0. F

hence contradiction by A26, VECTSP_1:25; :: thesis: verum

(RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

(RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

Line ((RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

(RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

A27: width A1 = F

A28: (Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

.= ((1_ F

.= (((1_ F

.= ((0. F

.= ((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 A4, FINSEQ_1:def 13;

A31: dom (Sgm N) = Seg (card N) by A4, 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_ F

(RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

Line ((RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

(RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

proof

thus
P
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_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,((Sgm N) /. i)) = 1_ F_{1}() )

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_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,((Sgm N) /. i)) = 1_ F_{1}()

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;

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

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;

end;

suppose A37:
i <= n
; :: thesis: (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,((Sgm N) /. i)) = 1_ F_{1}()

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_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,((Sgm N) /. i)) =
A1 * (i,((Sgm N) /. i))
by A19, A36, MATRIX11:def 3

.= 1_ F_{1}()
by A12, A33, A37
;

:: thesis: verum

end;hence (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

.= 1_ F

:: thesis: verum

suppose A38:
i = n + 1
; :: thesis: (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,((Sgm N) /. i)) = 1_ F_{1}()

A39:
A1 * (i,((Sgm N) /. i)) <> 0. F_{1}()
by A15, A33;

( (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (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_ F_{1}())) * (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_ F_{1}()
by A39, VECTSP_1:def 10
;

:: thesis: verum

end;( (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

hence (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

.= 1_ F

:: thesis: verum

(RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

Line ((RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

(RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

thus Segm ((RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

(RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

Line ((RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

(RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

proof

thus
for i being Nat st i in Seg (card N) holds
A40:
Indices A1 = Indices (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (Line (A1,(n + 1)))))))
by MATRIX_0:26;

let i be Nat; :: according to MATRIX_1:def 6 :: thesis: for b_{1} being set holds

( not [i,b_{1}] in Indices (Segm ((RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))),(Seg (card N)),N)) * (i,b_{1}) = 0. F_{1}() or i = b_{1} )

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_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))),(Seg (card N)),N)) * (i,j) = 0. F_{1}() 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_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))),(Seg (card N)),N)) * (i,j) <> 0. F_{1}()
; :: 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_ F_{1}())) * (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_ F_{1}())) * (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_ F_{1}())) * (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_ F_{1}())) * (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: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_ F_{1}())) * (Line (A1,(n + 1))))))),(Seg (card N)),N)) = Indices (Segm (A1,(Seg (card N)),N))
by MATRIX_0:26;

end;let i be Nat; :: according to MATRIX_1:def 6 :: thesis: for b

( not [i,b

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

assume that

A41: [i,j] in Indices (Segm ((RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

A42: (Segm ((RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

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

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

( 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: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_ F

per cases
( I = n + 1 or I <> n + 1 )
;

end;

suppose A48:
I = n + 1
; :: thesis: i = j

thus
i = j
:: thesis: verum

end;proof

assume A49:
i <> j
; :: thesis: contradiction

( (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (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_ F_{1}())) * (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. F_{1}())
by A14, A41, A47, A49

.= 0. F_{1}()
;

hence contradiction by A41, A42, A43, MATRIX13:def 1; :: thesis: verum

end;( (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

then (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

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

.= 0. F

hence contradiction by A41, A42, A43, MATRIX13:def 1; :: thesis: verum

suppose
I <> n + 1
; :: thesis: i = j

then (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (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;.= (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

(RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

Line ((RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

(RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

proof

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_ F
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_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,((Sgm N) /. i)) <> 0. F_{1}() )

assume A50: i in Seg (card N) ; :: thesis: (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,((Sgm N) /. i)) <> 0. F_{1}()

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

end;assume A50: i in Seg (card N) ; :: thesis: (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

( (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 )
;

end;

suppose
i = n + 1
; :: thesis: (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,((Sgm N) /. i)) <> 0. F_{1}()

hence
(RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,((Sgm N) /. i)) <> 0. F_{1}()
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_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,((Sgm N) /. i)) <> 0. F_{1}()

then
(RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,((Sgm N) /. i)) <> 0. F_{1}()
by A15, A50; :: thesis: verum

end;hence (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

Line ((RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

(RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

proof

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_ F
A52:
( dom (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (Line (A1,(n + 1))))))) = Seg (len (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (Line (A1,(n + 1)))))))) & len (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (Line (A1,(n + 1))))))) = F_{2}() )
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_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))),i) = F_{3}() |-> (0. F_{1}()) )

assume A53: ( i in dom (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (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_ F_{1}())) * (Line (A1,(n + 1))))))),i) = F_{3}() |-> (0. F_{1}())

thus Line ((RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (Line (A1,(n + 1))))))),i) =
Line (A1,i)
by A10, A53, A52, MATRIX11:28

.= F_{3}() |-> (0. F_{1}())
by A16, A29, A18, A53, A52
; :: thesis: verum

end;let i be Nat; :: thesis: ( i in dom (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

assume A53: ( i in dom (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

thus Line ((RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

.= F

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

A56: j < (Sgm N) . i ; :: thesis: (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

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

end;

suppose
i = n + 1
; :: thesis: (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,j) = 0. F_{1}()

then
( (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (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_ F_{1}())) * (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. F_{1}())
by A17, A27, A23, A54, A55, A56

.= 0. F_{1}()
;

:: thesis: verum

end;hence (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F

.= ((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") * (0. F

.= 0. F

:: thesis: verum

suppose
i <> n + 1
; :: thesis: (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,j) = 0. F_{1}()

hence (RLine (A1,(n + 1),((Line (A1,(n + 1))) + ((((A1 * ((n + 1),((Sgm N) /. (n + 1)))) ") - (1_ F_{1}())) * (Line (A1,(n + 1))))))) * (i,j) =
A1 * (i,j)
by A19, A57, MATRIX11:def 3

.= 0. F_{1}()
by A17, A27, A23, A54, A55, A56
;

:: thesis: verum

end;.= 0. F

:: thesis: verum

A9 * (i,((Sgm N) /. i)) = 1_ F

then A58: S

for n being Nat holds S

then consider A being Matrix of F

A59: the_rank_of F

A60: for i being Nat st i in Seg (card N) & i <= card N holds

A * (i,((Sgm N) /. i)) = 1_ F

A61: P

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

A63: ( ( for i being Nat st i in dom A & i > card N holds

Line (A,i) = F

A * (i,j) = 0. F

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

( N c= Seg F

Line (A,i) = F

A * (i,j) = 0. F

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

( N c= Seg F

Line (A,i) = F

A * (i,j) = 0. F

take N ; :: thesis: ( N c= Seg F

Line (A,i) = F

A * (i,j) = 0. F

thus ( N c= Seg F

Line (A,i) = F

A * (i,j) = 0. F

set S = Segm (A,(Seg (card N)),N);

A64: card (Seg (card N)) = card N by FINSEQ_1:57;

then A65: Indices (1. (F

now :: thesis: for i, j being Nat st [i,j] in Indices (1. (F_{1}(),(card N))) holds

(Segm (A,(Seg (card N)),N)) * (i,j) = (1. (F_{1}(),(card N))) * (i,j)

hence
( Segm (A,(Seg (card N)),N) = 1. (F(Segm (A,(Seg (card N)),N)) * (i,j) = (1. (F

A66:
dom (Sgm N) = Seg (the_rank_of F_{5}())
by A4, A5, FINSEQ_3:40;

let i, j be Nat; :: thesis: ( [i,j] in Indices (1. (F_{1}(),(card N))) implies (Segm (A,(Seg (card N)),N)) * (i,j) = (1. (F_{1}(),(card N))) * (i,j) )

assume A67: [i,j] in Indices (1. (F_{1}(),(card N)))
; :: thesis: (Segm (A,(Seg (card N)),N)) * (i,j) = (1. (F_{1}(),(card N))) * (i,j)

A68: j in Seg (the_rank_of F_{5}())
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 F_{5}())
by A7, A67, ZFMISC_1:87;

then A70: (idseq (the_rank_of F_{5}())) . i9 = i9
by FINSEQ_2:49;

A71: i <= the_rank_of F_{5}()
by A69, FINSEQ_1:1;

A72: (Segm (A,(Seg (card N)),N)) * (i,j) = A * (((Sgm (Seg (the_rank_of F_{5}()))) . 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 ;

_{1}(),(card N))) * (i,j)
; :: thesis: verum

end;let i, j be Nat; :: thesis: ( [i,j] in Indices (1. (F

assume A67: [i,j] in Indices (1. (F

A68: j in Seg (the_rank_of F

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

A69: i in Seg (the_rank_of F

then A70: (idseq (the_rank_of F

A71: i <= the_rank_of F

A72: (Segm (A,(Seg (card N)),N)) * (i,j) = A * (((Sgm (Seg (the_rank_of F

.= 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. (F_{1}(),(card N))) * (i,j)end;

hence
(Segm (A,(Seg (card N)),N)) * (i,j) = (1. (Fper cases
( i9 = j9 or i9 <> j9 )
;

end;

Line (A,i) = F

A * (i,j) = 0. F