matrix14.miz

begin

 reserve k,n,m,i,j for Element of NAT ,

K for Field;

 definition

 let K be non empty ZeroStr, n;

 :: MATRIX14:def1

 func 0* (K,n) -> FinSequence of K equals (n |-> ( 0. K));

 coherence ;

 end

 definition

 let K be non empty ZeroStr;

 let n;

 :: original: 0*

 redefine

 func 0* (K,n) -> Element of (n -tuples_on the carrier of K) ;

 coherence ;

 end

 reserve L for non empty addLoopStr;

 theorem :: MATRIX14:1



 Th1: for x be FinSequence of L holds x is Element of (( len x) -tuples_on the carrier of L)

 proof

 let x be FinSequence of L;

 x is Element of (the carrier of L * ) by FINSEQ_1:def 11;

 then x in { s where s be Element of (the carrier of L * ) : ( len s) = ( len x) };

 hence thesis by FINSEQ_2:def 4;

 end;

 theorem :: MATRIX14:2



 Th2: for x1,x2 be FinSequence of L st ( len x1) = ( len x2) holds ( len (x1 + x2)) = ( len x1)

 proof

 let x1,x2 be FinSequence of L;

 set n = ( len x1);

 reconsider z1 = x1 as Element of (( len x1) -tuples_on the carrier of L) by FINSEQ_2: 92;

 assume ( len x1) = ( len x2);

 then

 reconsider z2 = x2 as Element of (n -tuples_on the carrier of L) by FINSEQ_2: 92;

 ( dom (z1 + z2)) = ( Seg n) by FINSEQ_2: 124;

 hence thesis by FINSEQ_1:def 3;

 end;

 theorem :: MATRIX14:3



 Th3: for x1,x2 be FinSequence of L st ( len x1) = ( len x2) holds ( len (x1 - x2)) = ( len x1)

 proof

 let x1,x2 be FinSequence of L;

 set n = ( len x1);

 reconsider z1 = x1 as Element of (( len x1) -tuples_on the carrier of L) by FINSEQ_2: 92;

 assume ( len x1) = ( len x2);

 then

 reconsider z2 = x2 as Element of (n -tuples_on the carrier of L) by FINSEQ_2: 92;

 ( dom (z1 - z2)) = ( Seg n) by FINSEQ_2: 124;

 hence thesis by FINSEQ_1:def 3;

 end;

 reserve G for non empty multLoopStr;

 theorem :: MATRIX14:4



 Th4: for x1,x2 be FinSequence of G, i st i in ( dom ( mlt (x1,x2))) holds (( mlt (x1,x2)) . i) = ((x1 /. i) * (x2 /. i)) & (( mlt (x1,x2)) /. i) = ((x1 /. i) * (x2 /. i))

 proof

 let x1,x2 be FinSequence of G, i;

 assume

 A1: i in ( dom ( mlt (x1,x2)));



 A2: ( mlt (x1,x2)) = (the multF of G .: (x1,x2)) by FVSUM_1:def 7;



 A3: ( rng x2) c= the carrier of G by FINSEQ_1:def 4;

 ( dom the multF of G) = [:the carrier of G, the carrier of G:] & ( rng x1) c= the carrier of G by FINSEQ_1:def 4, FUNCT_2:def 1;

 then [:( rng x1), ( rng x2):] c= ( dom the multF of G) by A3, ZFMISC_1: 96;

 then

 A4: ( dom ( mlt (x1,x2))) = (( dom x1) /\ ( dom x2)) by A2, FUNCOP_1: 69;

 then i in ( dom x2) by A1, XBOOLE_0:def 4;

 then

 A5: (x2 /. i) = (x2 . i) by PARTFUN1:def 6;

 i in ( dom x1) by A1, A4, XBOOLE_0:def 4;

 then (x1 /. i) = (x1 . i) by PARTFUN1:def 6;

 hence (( mlt (x1,x2)) . i) = ((x1 /. i) * (x2 /. i)) by A1, A5, FVSUM_1: 60;

 hence thesis by A1, PARTFUN1:def 6;

 end;

 theorem :: MATRIX14:5



 Th5: for x1,x2 be FinSequence of L, i be Nat st ( len x1) = ( len x2) & 1 <= i & i <= ( len x1) holds ((x1 + x2) . i) = ((x1 /. i) + (x2 /. i)) & ((x1 - x2) . i) = ((x1 /. i) - (x2 /. i))

 proof

 let x1,x2 be FinSequence of L, i be Nat;

 assume that

 A1: ( len x1) = ( len x2) and

 A2: 1 <= i & i <= ( len x1);

 reconsider x10 = x1, x20 = x2 as Element of (( len x1) -tuples_on the carrier of L) by A1, Th1;



 A3: (x10 /. i) = (x10 . i) & (x20 /. i) = (x20 . i) by A1, A2, FINSEQ_4: 15;

 i in ( Seg ( len x1)) by A2, FINSEQ_1: 1;

 then i in ( Seg ( len (x1 + x2))) by A1, Th2;

 then i in ( dom (x1 + x2)) by FINSEQ_1:def 3;

 hence ((x1 + x2) . i) = ((x1 /. i) + (x2 /. i)) by A3, FVSUM_1: 17;

 i in ( Seg ( len x1)) by A2, FINSEQ_1: 1;

 then i in ( Seg ( len (x1 - x2))) by A1, Th3;

 then i in ( dom (x1 - x2)) by FINSEQ_1:def 3;

 hence thesis by A3, FVSUM_1: 32;

 end;

 theorem :: MATRIX14:6



 Th6: for a be Element of K, x be FinSequence of K holds ( - (a * x)) = (( - a) * x) & ( - (a * x)) = (a * ( - x))

 proof

 let a be Element of K, x be FinSequence of K;

 set n = ( len x);

 reconsider x0 = x as Element of (n -tuples_on the carrier of K) by Th1;

 reconsider y = (a * x0) as Element of (n -tuples_on the carrier of K);



 thus ( - (a * x)) = (( - ( 1_ K)) * y) by FVSUM_1: 59

 .= ((( - ( 1_ K)) * a) * x0) by FVSUM_1: 54

 .= (( - (( 1_ K) * a)) * x0) by VECTSP_1: 8

 .= (( - a) * x);



 thus ( - (a * x)) = (( - ( 1_ K)) * y) by FVSUM_1: 59

 .= ((( - ( 1_ K)) * a) * x0) by FVSUM_1: 54

 .= (a * (( - ( 1_ K)) * x0)) by FVSUM_1: 54

 .= (a * ( - x)) by FVSUM_1: 59;

 end;

 theorem :: MATRIX14:7



 Th7: for x1,x2,y1,y2 be FinSequence of G st ( len x1) = ( len x2) & ( len y1) = ( len y2) holds ( mlt ((x1 ^ y1),(x2 ^ y2))) = (( mlt (x1,x2)) ^ ( mlt (y1,y2)))

 proof

 let x1,x2,y1,y2 be FinSequence of G;

 assume that

 A1: ( len x1) = ( len x2) and

 A2: ( len y1) = ( len y2);



 A3: (the multF of G .: ((x1 ^ y1),(x2 ^ y2))) = (the multF of G * <:(x1 ^ y1), (x2 ^ y2):>) by FUNCOP_1:def 3;



 A4: ( dom (x1 ^ y1)) = ( Seg ( len (x1 ^ y1))) by FINSEQ_1:def 3;



 A5: ( rng (x2 ^ y2)) c= the carrier of G by FINSEQ_1:def 4;

 ( dom the multF of G) = [:the carrier of G, the carrier of G:] & ( rng (x1 ^ y1)) c= the carrier of G by FINSEQ_1:def 4, FUNCT_2:def 1;

 then [:( rng (x1 ^ y1)), ( rng (x2 ^ y2)):] c= ( dom the multF of G) by A5, ZFMISC_1: 96;

 then

 A6: ( dom (the multF of G * <:(x1 ^ y1), (x2 ^ y2):>)) = (( dom (x1 ^ y1)) /\ ( dom (x2 ^ y2))) by A3, FUNCOP_1: 69;



 A7: ( len (x2 ^ y2)) = (( len x2) + ( len y2)) by FINSEQ_1: 22;

 ( dom (x2 ^ y2)) = ( Seg ( len (x2 ^ y2))) by FINSEQ_1:def 3;

 then ( dom (x1 ^ y1)) = ( dom (x2 ^ y2)) by A1, A2, A7, A4, FINSEQ_1: 22;

 then

 A8: ( dom ( mlt ((x1 ^ y1),(x2 ^ y2)))) = ( dom (x1 ^ y1)) by A3, A6, FVSUM_1:def 7;



 A9: (the multF of G .: (y1,y2)) = (the multF of G * <:y1, y2:>) by FUNCOP_1:def 3;



 A10: ( dom the multF of G) = [:the carrier of G, the carrier of G:] by FUNCT_2:def 1;

 ( rng y1) c= the carrier of G & ( rng y2) c= the carrier of G by FINSEQ_1:def 4;

 then [:( rng y1), ( rng y2):] c= ( dom the multF of G) by A10, ZFMISC_1: 96;

 then

 A11: ( dom (the multF of G * <:y1, y2:>)) = (( dom y1) /\ ( dom y2)) by A9, FUNCOP_1: 69;

 ( dom y2) = ( Seg ( len y1)) by A2, FINSEQ_1:def 3

 .= ( dom y1) by FINSEQ_1:def 3;

 then

 A12: ( dom ( mlt (y1,y2))) = ( dom y1) by A9, A11, FVSUM_1:def 7;

 then ( dom ( mlt (y1,y2))) = ( Seg ( len y1)) by FINSEQ_1:def 3;

 then

 A13: ( len ( mlt (y1,y2))) = ( len y1) by FINSEQ_1:def 3;



 A14: (the multF of G .: (x1,x2)) = (the multF of G * <:x1, x2:>) by FUNCOP_1:def 3;

 ( rng x1) c= the carrier of G & ( rng x2) c= the carrier of G by FINSEQ_1:def 4;

 then [:( rng x1), ( rng x2):] c= ( dom the multF of G) by A10, ZFMISC_1: 96;

 then

 A15: ( dom (the multF of G * <:x1, x2:>)) = (( dom x1) /\ ( dom x2)) by A14, FUNCOP_1: 69;



 A16: ( len (x1 ^ y1)) = (( len x1) + ( len y1)) by FINSEQ_1: 22;

 ( dom x2) = ( Seg ( len x1)) by A1, FINSEQ_1:def 3

 .= ( dom x1) by FINSEQ_1:def 3;

 then

 A17: ( dom ( mlt (x1,x2))) = ( dom x1) by A14, A15, FVSUM_1:def 7;

 then

 A18: ( dom ( mlt (x1,x2))) = ( Seg ( len x1)) by FINSEQ_1:def 3;



 A19: for i be Nat st 1 <= i & i <= ( len ( mlt ((x1 ^ y1),(x2 ^ y2)))) holds (( mlt ((x1 ^ y1),(x2 ^ y2))) . i) = ((( mlt (x1,x2)) ^ ( mlt (y1,y2))) . i)

 proof

 let i be Nat;

 assume that

 A20: 1 <= i and

 A21: i <= ( len ( mlt ((x1 ^ y1),(x2 ^ y2))));

 i in ( Seg ( len ( mlt ((x1 ^ y1),(x2 ^ y2))))) by A20, A21, FINSEQ_1: 1;

 then

 A22: i in ( dom ( mlt ((x1 ^ y1),(x2 ^ y2)))) by FINSEQ_1:def 3;

 then i <= ( len (x1 ^ y1)) by A4, A8, FINSEQ_1: 1;

 then

 A23: ((x1 ^ y1) /. i) = ((x1 ^ y1) . i) by A20, FINSEQ_4: 15;

 i <= ( len (x2 ^ y2)) by A1, A2, A16, A7, A4, A8, A22, FINSEQ_1: 1;

 then

 A24: ((x2 ^ y2) /. i) = ((x2 ^ y2) . i) by A20, FINSEQ_4: 15;



 A25: i <= (( len x1) + ( len y1)) by A16, A4, A8, A22, FINSEQ_1: 1;

 now

 per cases ;

 suppose

 A26: i <= ( len x1);

 then

 A27: i in ( Seg ( len x1)) by A20, FINSEQ_1: 1;

 then

 A28: i in ( dom x1) by FINSEQ_1:def 3;

 i in ( dom x2) by A1, A27, FINSEQ_1:def 3;

 then

 A29: ((x2 ^ y2) . i) = (x2 . i) by FINSEQ_1:def 7;



 A30: i in ( dom ( mlt (x1,x2))) by A17, A27, FINSEQ_1:def 3;



 then

 A31: ((( mlt (x1,x2)) ^ ( mlt (y1,y2))) . i) = (( mlt (x1,x2)) . i) by FINSEQ_1:def 7

 .= ((x1 /. i) * (x2 /. i)) by A30, Th4;

 (x1 /. i) = (x1 . i) & (x2 /. i) = (x2 . i) by A1, A20, A26, FINSEQ_4: 15;

 hence (((x1 ^ y1) /. i) * ((x2 ^ y2) /. i)) = ((( mlt (x1,x2)) ^ ( mlt (y1,y2))) . i) by A23, A24, A28, A29, A31, FINSEQ_1:def 7;

 end;

 suppose

 A32: i > ( len x1);

 i <= ( len (x2 ^ y2)) by A1, A2, A16, A7, A4, A8, A22, FINSEQ_1: 1;

 then

 A33: ((x2 ^ y2) /. i) = ((x2 ^ y2) . i) by A20, FINSEQ_4: 15;

 i <= ( len (x1 ^ y1)) by A4, A8, A22, FINSEQ_1: 1;

 then

 A34: ((x1 ^ y1) /. i) = ((x1 ^ y1) . i) by A20, FINSEQ_4: 15;

 set k = (i -' ( len x1));



 A35: k = (i - ( len x1)) by A32, XREAL_1: 233;

 then

 A36: i = (( len x1) + k);

 (i - ( len x1)) <= ((( len x1) + ( len y1)) - ( len x1)) by A25, XREAL_1: 13;

 then

 A37: k <= ( len y1) by A32, XREAL_1: 233;

 k > 0 by A32, A35, XREAL_1: 50;

 then

 A38: ( 0 + 1) <= k by NAT_1: 13;

 then

 A39: k in ( Seg ( len y1)) by A37, FINSEQ_1: 1;

 then

 A40: k in ( dom ( mlt (y1,y2))) by A12, FINSEQ_1:def 3;

 i = (( len ( mlt (x1,x2))) + k) by A18, A36, FINSEQ_1:def 3;



 then

 A41: ((( mlt (x1,x2)) ^ ( mlt (y1,y2))) . i) = (( mlt (y1,y2)) . k) by A40, FINSEQ_1:def 7

 .= ((y1 /. k) * (y2 /. k)) by A40, Th4;

 k in ( dom y1) by A39, FINSEQ_1:def 3;

 then

 A42: ((x1 ^ y1) . i) = (y1 . k) by A36, FINSEQ_1:def 7;

 k in ( Seg ( len y1)) by A38, A37, FINSEQ_1: 1;

 then

 A43: k in ( dom y2) by A2, FINSEQ_1:def 3;

 (y1 /. k) = (y1 . k) & (y2 /. k) = (y2 . k) by A2, A38, A37, FINSEQ_4: 15;

 hence (((x1 ^ y1) /. i) * ((x2 ^ y2) /. i)) = ((( mlt (x1,x2)) ^ ( mlt (y1,y2))) . i) by A1, A36, A43, A42, A34, A33, A41, FINSEQ_1:def 7;

 end;

 end;

 hence thesis by A22, Th4;

 end;

 ( len ( mlt ((x1 ^ y1),(x2 ^ y2)))) = ( len (x1 ^ y1)) by A4, A8, FINSEQ_1:def 3

 .= (( len x1) + ( len y1)) by FINSEQ_1: 22;

 then ( len ( mlt ((x1 ^ y1),(x2 ^ y2)))) = (( len ( mlt (x1,x2))) + ( len ( mlt (y1,y2)))) by A18, A13, FINSEQ_1:def 3;

 then ( len ( mlt ((x1 ^ y1),(x2 ^ y2)))) = ( len (( mlt (x1,x2)) ^ ( mlt (y1,y2)))) by FINSEQ_1: 22;

 hence thesis by A19, FINSEQ_1: 14;

 end;

 notation

 let K;

 let e1,e2 be FinSequence of K;

 synonym |(e1,e2)| for e1 "*" e2;

 end

 theorem :: MATRIX14:8



 Th8: for x,y be FinSequence of K, a be Element of K st ( len x) = ( len y) holds ( mlt ((a * x),y)) = (a * ( mlt (x,y))) & ( mlt (x,(a * y))) = (a * ( mlt (x,y)))

 proof

 let x,y be FinSequence of K, a be Element of K;

 assume ( len x) = ( len y);

 then

 reconsider y0 = y as Element of (( len x) -tuples_on the carrier of K) by Th1;

 reconsider x0 = x as Element of (( len x) -tuples_on the carrier of K) by Th1;



 thus ( mlt ((a * x),y)) = (a * ( mlt (x0,y0))) by FVSUM_1: 69

 .= (a * ( mlt (x,y)));



 thus ( mlt (x,(a * y))) = (a * ( mlt (x0,y0))) by FVSUM_1: 69

 .= (a * ( mlt (x,y)));

 end;

 theorem :: MATRIX14:9

 for x,y be FinSequence of K, a be Element of K st ( len x) = ( len y) holds |((a * x), y)| = (a * |(x, y)|)

 proof

 let x,y be FinSequence of K, a be Element of K;

 assume ( len x) = ( len y);

 then ( Sum ( mlt ((a * x),y))) = ( Sum (a * ( mlt (x,y)))) by Th8;

 then ( Sum ( mlt ((a * x),y))) = (a * ( Sum ( mlt (x,y)))) by FVSUM_1: 73;

 then ( Sum ( mlt ((a * x),y))) = (a * |(x, y)|) by FVSUM_1:def 9;

 hence thesis by FVSUM_1:def 9;

 end;

 theorem :: MATRIX14:10



 Th10: for x,y be FinSequence of K, a be Element of K st ( len x) = ( len y) holds |(x, (a * y))| = (a * |(x, y)|)

 proof

 let x,y be FinSequence of K, a be Element of K;

 assume ( len x) = ( len y);

 then ( Sum ( mlt (x,(a * y)))) = ( Sum (a * ( mlt (x,y)))) by Th8;

 then ( Sum ( mlt (x,(a * y)))) = (a * ( Sum ( mlt (x,y)))) by FVSUM_1: 73;

 then ( Sum ( mlt (x,(a * y)))) = (a * |(x, y)|) by FVSUM_1:def 9;

 hence thesis by FVSUM_1:def 9;

 end;

 theorem :: MATRIX14:11



 Th11: for x,y1,y2 be FinSequence of K, a be Element of K st ( len x) = ( len y1) & ( len x) = ( len y2) holds |(x, (y1 + y2))| = ( |(x, y1)| + |(x, y2)|)

 proof

 let x,y1,y2 be FinSequence of K, a be Element of K;

 reconsider x0 = x as Element of (( len x) -tuples_on the carrier of K) by Th1;

 assume

 A1: ( len x) = ( len y1) & ( len x) = ( len y2);

 then

 reconsider y10 = y1, y20 = y2 as Element of (( len x) -tuples_on the carrier of K) by Th1;

 ( Sum ( mlt (x,(y1 + y2)))) = ( Sum (( mlt (x0,y10)) + ( mlt (x0,y20)))) by A1, MATRIX_4: 57;

 then ( Sum ( mlt (x,(y1 + y2)))) = (( Sum ( mlt (x0,y10))) + ( Sum ( mlt (x0,y20)))) by FVSUM_1: 76;

 then ( Sum ( mlt (x,(y1 + y2)))) = (( Sum ( mlt (x,y1))) + |(x, y2)|) by FVSUM_1:def 9;

 then ( Sum ( mlt (x,(y1 + y2)))) = ( |(x, y1)| + |(x, y2)|) by FVSUM_1:def 9;

 hence thesis by FVSUM_1:def 9;

 end;

 theorem :: MATRIX14:12



 Th12: for x1,x2,y1,y2 be FinSequence of K st ( len x1) = ( len x2) & ( len y1) = ( len y2) holds |((x1 ^ y1), (x2 ^ y2))| = ( |(x1, x2)| + |(y1, y2)|)

 proof

 let x1,x2,y1,y2 be FinSequence of K;



 A1: ( Sum (( mlt (x1,x2)) ^ ( mlt (y1,y2)))) = (( Sum ( mlt (x1,x2))) + ( Sum ( mlt (y1,y2)))) by RLVECT_1: 41;

 assume ( len x1) = ( len x2) & ( len y1) = ( len y2);

 then ( Sum ( mlt ((x1 ^ y1),(x2 ^ y2)))) = (( Sum ( mlt (x1,x2))) + ( Sum ( mlt (y1,y2)))) by A1, Th7;

 then |((x1 ^ y1), (x2 ^ y2))| = (( Sum ( mlt (x1,x2))) + ( Sum ( mlt (y1,y2)))) by FVSUM_1:def 9;

 then |((x1 ^ y1), (x2 ^ y2))| = (( Sum ( mlt (x1,x2))) + |(y1, y2)|) by FVSUM_1:def 9;

 hence thesis by FVSUM_1:def 9;

 end;

 theorem :: MATRIX14:13



 Th13: for p1 be Element of (n -tuples_on the carrier of K) holds ( mlt (p1,(n |-> ( 0. K)))) = (n |-> ( 0. K))

 proof

 let p1 be Element of (n -tuples_on the carrier of K);



 thus ( mlt (p1,(n |-> ( 0. K)))) = ( mlt (p1,(( 0. K) * ( 0* (K,n))))) by FVSUM_1: 58

 .= (( 0. K) * ( mlt (p1,( 0* (K,n))))) by FVSUM_1: 69

 .= (n |-> ( 0. K)) by FVSUM_1: 58;

 end;

 notation

 let n;

 let K;

 let A be Matrix of n, K;

 synonym Inv A for A ~ ;

 end

 begin

 theorem :: MATRIX14:14



 Th14: ( 1. (K, 0 )) = ( 0. (K, 0 )) & ( 1. (K, 0 )) = {}

 proof



 A1: ( len ( 1. (K, 0 ))) = 0 by MATRIX_0: 24;

 hence ( 1. (K, 0 )) = ( 0. (K, 0 ));

 thus thesis by A1;

 end;

 theorem :: MATRIX14:15



 Th15: for A be Matrix of 0 , K holds A = {} & A = ( 1. (K, 0 )) & A = ( 0. (K, 0 ))

 proof

 let A be Matrix of 0 , K;



 A1: ( len A) = 0 by MATRIX_0: 24;

 hence A = {} ;

 hence A = ( 1. (K, 0 )) by Th14;

 thus thesis by A1;

 end;

 theorem :: MATRIX14:16

 for A be Matrix of 0 , K holds A is invertible

 proof

 let A be Matrix of 0 , K;

 (A * A) = ( 1. (K, 0 )) by Th15;

 then A is_reverse_of A by MATRIX_6:def 2;

 hence thesis by MATRIX_6:def 3;

 end;

 theorem :: MATRIX14:17



 Th17: for A,B,C be Matrix of n, K holds ((A * B) * C) = (A * (B * C))

 proof

 let A,B,C be Matrix of n, K;



 A1: ( width B) = n & ( len C) = n by MATRIX_0: 24;

 ( width A) = n & ( len B) = n by MATRIX_0: 24;

 hence thesis by A1, MATRIX_3: 33;

 end;

 theorem :: MATRIX14:18



 Th18: for A,B be Matrix of n, K holds A is invertible & B = (A ~ ) iff (B * A) = ( 1. (K,n)) & (A * B) = ( 1. (K,n))

 proof

 let A,B be Matrix of n, K;

 hereby

 assume A is invertible & B = (A ~ );

 then B is_reverse_of A by MATRIX_6:def 4;

 hence (B * A) = ( 1. (K,n)) & (A * B) = ( 1. (K,n)) by MATRIX_6:def 2;

 end;

 hereby

 assume (B * A) = ( 1. (K,n)) & (A * B) = ( 1. (K,n));

 then

 A1: B is_reverse_of A by MATRIX_6:def 2;

 hence A is invertible by MATRIX_6:def 3;

 hence B = (A ~ ) by A1, MATRIX_6:def 4;

 end;

 end;

 theorem :: MATRIX14:19



 Th19: for A be Matrix of n, K holds A is invertible iff ex B be Matrix of n, K st (B * A) = ( 1. (K,n)) & (A * B) = ( 1. (K,n))

 proof

 let A be Matrix of n, K;

 thus A is invertible implies ex B be Matrix of n, K st (B * A) = ( 1. (K,n)) & (A * B) = ( 1. (K,n))

 proof

 assume A is invertible;

 then ((A ~ ) * A) = ( 1. (K,n)) & (A * (A ~ )) = ( 1. (K,n)) by Th18;

 hence thesis;

 end;

 thus thesis by Th18;

 end;

 theorem :: MATRIX14:20



 Th20: for x be FinSequence of K holds |(x, ( 0* (K,( len x))))| = ( 0. K)

 proof

 let x be FinSequence of K;

 set n = ( len x);

 reconsider p1 = x as Element of (n -tuples_on the carrier of K) by FINSEQ_2: 92;

 |(x, ( 0* (K,n)))| = ( Sum ( mlt (p1,( 0* (K,n))))) by FVSUM_1:def 9

 .= ( Sum ( 0* (K,n))) by Th13

 .= ( 0. K) by MATRIX_3: 11;

 hence thesis;

 end;

 theorem :: MATRIX14:21



 Th21: for x be FinSequence of K holds |(( 0* (K,( len x))), x)| = ( 0. K)

 proof

 let x be FinSequence of K;



 thus |(( 0* (K,( len x))), x)| = |(x, ( 0* (K,( len x))))| by FVSUM_1: 90

 .= ( 0. K) by Th20;

 end;

 theorem :: MATRIX14:22



 Th22: for a be Element of K holds |( <*( 0. K)*>, <*a*>)| = ( 0. K)

 proof

 let a be Element of K;



 A1: ( len <*a*>) = 1 by FINSEQ_1: 39;



 thus |( <*( 0. K)*>, <*a*>)| = |(( 0* (K,1)), <*a*>)| by FINSEQ_2: 59

 .= ( 0. K) by A1, Th21;

 end;

 definition

 let K;

 let n,i be Nat;

 :: MATRIX14:def2

 func Base_FinSeq (K,n,i) -> FinSequence of K equals ( Replace ((n |-> ( 0. K)),i,( 1. K)));

 coherence ;

 end

 theorem :: MATRIX14:23



 Th23: for n,i be Nat holds ( len ( Base_FinSeq (K,n,i))) = n

 proof

 let n,i be Nat;

 ( len ( Replace ((n |-> ( 0. K)),i,( 1. K)))) = ( len (n |-> ( 0. K))) by FINSEQ_7: 5

 .= n by CARD_1:def 7;

 hence thesis;

 end;

 theorem :: MATRIX14:24



 Th24: for i,n be Nat st 1 <= i & i <= n holds (( Base_FinSeq (K,n,i)) . i) = ( 1. K)

 proof

 let i,n be Nat;

 assume

 A1: 1 <= i & i <= n;



 A2: ( len (n |-> ( 0. K))) = n by CARD_1:def 7;

 ( len ( Replace ((n |-> ( 0. K)),i,( 1. K)))) = ( len (n |-> ( 0. K))) by FINSEQ_7: 5

 .= n by CARD_1:def 7;



 hence (( Base_FinSeq (K,n,i)) . i) = (( Replace ((n |-> ( 0. K)),i,( 1. K))) /. i) by A1, FINSEQ_4: 15

 .= ( 1. K) by A1, A2, FINSEQ_7: 8;

 end;

 theorem :: MATRIX14:25



 Th25: for i,j,n be Nat st 1 <= j & j <= n & i <> j holds (( Base_FinSeq (K,n,i)) . j) = ( 0. K)

 proof

 let i,j,n be Nat;

 assume that

 A1: 1 <= j & j <= n and

 A2: i <> j;



 A3: j in ( Seg n) by A1, FINSEQ_1: 1;



 A4: ( len (n |-> ( 0. K))) = n by CARD_1:def 7;

 ( len ( Replace ((n |-> ( 0. K)),i,( 1. K)))) = ( len (n |-> ( 0. K))) by FINSEQ_7: 5

 .= n by CARD_1:def 7;



 hence (( Base_FinSeq (K,n,i)) . j) = (( Replace ((n |-> ( 0. K)),i,( 1. K))) /. j) by A1, FINSEQ_4: 15

 .= ((n |-> ( 0. K)) /. j) by A1, A2, A4, FINSEQ_7: 10

 .= ((n |-> ( 0. K)) . j) by A1, A4, FINSEQ_4: 15

 .= ( 0. K) by A3, FINSEQ_2: 57;

 end;

 theorem :: MATRIX14:26



 Th26: for i,n be Nat st 1 <= i & i <= n holds (( 1. (K,n)) . i) = ( Base_FinSeq (K,n,i))

 proof

 let i,n be Nat;

 assume

 A1: 1 <= i & i <= n;

 then 1 <= n by XXREAL_0: 2;

 then [i, 1] in ( Indices ( 1. (K,n))) by A1, MATRIX_0: 31;

 then

 consider q be FinSequence of K such that

 A2: q = (( 1. (K,n)) . i) and (( 1. (K,n)) * (i,1)) = (q . 1) by MATRIX_0:def 5;

 ( len ( 1. (K,n))) = n by MATRIX_0: 24;

 then i in ( dom ( 1. (K,n))) by A1, FINSEQ_3: 25;

 then q in ( rng ( 1. (K,n))) by A2, FUNCT_1:def 3;

 then

 A3: ( len q) = n by MATRIX_0:def 2;



 A4: for j be Nat st 1 <= j & j <= n holds (q . j) = (( Base_FinSeq (K,n,i)) . j)

 proof

 let j be Nat;

 assume

 A5: 1 <= j & j <= n;

 then

 A6: [i, j] in ( Indices ( 1. (K,n))) by A1, MATRIX_0: 31;

 then

 A7: ex q0 be FinSequence of K st q0 = (( 1. (K,n)) . i) & (( 1. (K,n)) * (i,j)) = (q0 . j) by MATRIX_0:def 5;

 per cases ;

 suppose

 A8: i = j;

 then (( 1. (K,n)) * (i,i)) = ( 1_ K) by A6, MATRIX_1:def 3;

 hence thesis by A1, A2, A7, A8, Th24;

 end;

 suppose

 A9: i <> j;

 then (q . j) = ( 0. K) by A2, A6, A7, MATRIX_1:def 3;

 hence thesis by A5, A9, Th25;

 end;

 end;

 ( len ( Base_FinSeq (K,n,i))) = n by Th23;

 hence thesis by A2, A3, A4, FINSEQ_1: 14;

 end;

 theorem :: MATRIX14:27



 Th27: for i, j st 1 <= i & i <= n & 1 <= j & j <= n holds (( 1. (K,n)) * (i,j)) = (( Base_FinSeq (K,n,i)) . j)

 proof

 let i, j;

 assume that

 A1: 1 <= i & i <= n and

 A2: 1 <= j & j <= n;

 [i, j] in ( Indices ( 1. (K,n))) by A1, A2, MATRIX_0: 31;

 then ex p3 be FinSequence of K st p3 = (( 1. (K,n)) . i) & (( 1. (K,n)) * (i,j)) = (p3 . j) by MATRIX_0:def 5;

 hence thesis by A1, Th26;

 end;

 theorem :: MATRIX14:28

 for A be Matrix of n, K holds A = ( 0. (K,n)) iff for i,j be Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds (A * (i,j)) = ( 0. K)

 proof

 let A be Matrix of n, K;

 thus A = ( 0. (K,n)) implies for i,j be Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds (A * (i,j)) = ( 0. K)

 proof

 set A2 = ( 0. (K,n)), B2 = ( 0. (K,n));

 set A3 = ( 0. (K,n,n));

 assume

 A1: A = ( 0. (K,n));

 let i,j be Element of NAT ;

 assume 1 <= i & i <= n & 1 <= j & j <= n;

 then [i, j] in ( Indices A2) by MATRIX_0: 31;

 then A3 = A2 & ((A2 + B2) * (i,j)) = ((A2 * (i,j)) + (B2 * (i,j))) by MATRIX_3:def 1, MATRIX_3:def 3;

 then (A2 * (i,j)) = ((A2 * (i,j)) + (A2 * (i,j))) by MATRIX_3: 4;



 then ((A2 * (i,j)) - (A2 * (i,j))) = ((A2 * (i,j)) + ((A2 * (i,j)) - (A2 * (i,j)))) by RLVECT_1: 28

 .= ((A2 * (i,j)) + ( 0. K)) by RLVECT_1: 15

 .= (A2 * (i,j)) by RLVECT_1: 4;

 hence thesis by A1, RLVECT_1: 15;

 end;



 A2: ( len A) = n by MATRIX_0: 24;



 A3: ( Indices A) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;



 A4: ( width A) = n by MATRIX_0: 24;

 assume

 A5: for i,j be Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds (A * (i,j)) = ( 0. K);

 for i,j be Nat st [i, j] in ( Indices A) holds (A * (i,j)) = ((A * (i,j)) + (A * (i,j)))

 proof

 let i,j be Nat;

 reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def 12;

 assume

 A6: [i, j] in ( Indices A);

 then j in ( Seg n) by A4, ZFMISC_1: 87;

 then

 A7: 1 <= j & j <= n by FINSEQ_1: 1;

 i in ( Seg n) by A3, A6, ZFMISC_1: 87;

 then 1 <= i & i <= n by FINSEQ_1: 1;

 then (A * (i0,j0)) = ( 0. K) by A5, A7;

 hence thesis by RLVECT_1: 4;

 end;

 then A = (A + A) by A2, MATRIX_3:def 3;

 then A = ( 0. (K,( len A),( width A))) by MATRIX_4: 6;

 hence thesis by A2, A4, MATRIX_3:def 1;

 end;

 theorem :: MATRIX14:29



 Th29: for A be Matrix of n, K holds A = ( 1. (K,n)) iff for i,j be Nat st 1 <= i & i <= n & 1 <= j & j <= n holds (A * (i,j)) = ( IFEQ (i,j,( 1. K),( 0. K)))

 proof

 let A be Matrix of n, K;



 A1: ( Indices A) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

 thus A = ( 1. (K,n)) implies for i,j be Nat st 1 <= i & i <= n & 1 <= j & j <= n holds (A * (i,j)) = ( IFEQ (i,j,( 1. K),( 0. K)))

 proof

 assume

 A2: A = ( 1. (K,n));

 let i,j be Nat;

 assume 1 <= i & i <= n & 1 <= j & j <= n;

 then

 A3: [i, j] in ( Indices A) by MATRIX_0: 31;

 per cases ;

 suppose

 A4: i = j;

 then (A * (i,j)) = ( 1. K) by A2, A3, MATRIX_1:def 3;

 hence thesis by A4, FUNCOP_1:def 8;

 end;

 suppose

 A5: i <> j;

 then (A * (i,j)) = ( 0. K) by A2, A3, MATRIX_1:def 3;

 hence thesis by A5, FUNCOP_1:def 8;

 end;

 end;



 A6: ( len ( 1. (K,n))) = n & ( width ( 1. (K,n))) = n by MATRIX_0: 24;



 A7: ( Indices ( 1. (K,n))) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;



 A8: ( width A) = n by MATRIX_0: 24;

 thus (for i,j be Nat st 1 <= i & i <= n & 1 <= j & j <= n holds (A * (i,j)) = ( IFEQ (i,j,( 1. K),( 0. K)))) implies A = ( 1. (K,n))

 proof

 assume

 A9: for i,j be Nat st 1 <= i & i <= n & 1 <= j & j <= n holds (A * (i,j)) = ( IFEQ (i,j,( 1. K),( 0. K)));



 A10: for i,j be Nat st [i, j] in ( Indices A) holds (A * (i,j)) = (( 1. (K,n)) * (i,j))

 proof

 let i,j be Nat;

 reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def 12;

 assume

 A11: [i, j] in ( Indices A);

 then j in ( Seg n) by A8, ZFMISC_1: 87;

 then

 A12: 1 <= j & j <= n by FINSEQ_1: 1;

 i in ( Seg n) by A1, A11, ZFMISC_1: 87;

 then 1 <= i & i <= n by FINSEQ_1: 1;

 then

 A13: (A * (i0,j0)) = ( IFEQ (i0,j0,( 1. K),( 0. K))) by A9, A12;

 per cases ;

 suppose

 A14: i0 = j0;

 then (A * (i0,j0)) = ( 1_ K) by A13, FUNCOP_1:def 8;

 hence thesis by A1, A7, A11, A14, MATRIX_1:def 3;

 end;

 suppose

 A15: i0 <> j0;

 then (A * (i0,j0)) = ( 0. K) by A13, FUNCOP_1:def 8;

 hence thesis by A1, A7, A11, A15, MATRIX_1:def 3;

 end;

 end;

 ( len A) = ( len ( 1. (K,n))) & ( width A) = ( width ( 1. (K,n))) by A6, MATRIX_0: 24;

 hence thesis by A10, MATRIX_0: 21;

 end;

 end;

 begin

 theorem :: MATRIX14:30



 Th30: for A,B be Matrix of n, K holds ((A * B) @ ) = ((B @ ) * (A @ ))

 proof

 let A,B be Matrix of n, K;

 per cases ;

 suppose

 A1: n <> 0 ;



 A2: ( width B) = n by MATRIX_0: 24;

 ( len B) = n & ( width A) = n by MATRIX_0: 24;

 hence thesis by A1, A2, MATRIX_3: 22;

 end;

 suppose

 A3: n = 0 ;



 hence ((A * B) @ ) = ( 1. (K,n)) by Th15

 .= ((B @ ) * (A @ )) by A3, Th15;

 end;

 end;

 theorem :: MATRIX14:31

 for A be Matrix of n, K st A is invertible holds (A @ ) is invertible & ((A @ ) ~ ) = ((A ~ ) @ )

 proof

 let A be Matrix of n, K;

 assume A is invertible;

 then

 consider B be Matrix of n, K such that

 A1: (B * A) = ( 1. (K,n)) and

 A2: (A * B) = ( 1. (K,n)) by Th19;

 ((A * B) @ ) = ((B @ ) * (A @ )) by Th30;

 then

 A3: ((B @ ) * (A @ )) = ( 1. (K,n)) by A2, MATRIX_6: 10;

 ((B * A) @ ) = ((A @ ) * (B @ )) by Th30;

 then

 A4: ((A @ ) * (B @ )) = ( 1. (K,n)) by A1, MATRIX_6: 10;

 B = (A ~ ) by A1, A2, Th18;

 hence thesis by A3, A4, Th18;

 end;

 theorem :: MATRIX14:32



 Th32: for x be FinSequence of K, a be Element of K st (ex i st 1 <= i & i <= ( len x) & (x . i) = a & (for j st j <> i & 1 <= j & j <= ( len x) holds (x . j) = ( 0. K))) holds ( Sum x) = a

 proof

 let x be FinSequence of K, a be Element of K;

 given i such that

 A1: 1 <= i and

 A2: i <= ( len x) and

 A3: (x . i) = a and

 A4: for j st j <> i & 1 <= j & j <= ( len x) holds (x . j) = ( 0. K);

 1 <= ( len x) by A1, A2, XXREAL_0: 2;

 then

 consider f be sequence of the carrier of K such that

 A5: (f . 1) = (x . 1) and

 A6: for n be Nat st 0 <> n & n < ( len x) holds (f . (n + 1)) = (the addF of K . ((f . n),(x . (n + 1)))) and

 A7: (the addF of K "**" x) = (f . ( len x)) by FINSOP_1:def 1;



 A8: for j be Nat st 1 <= j & j < i holds (f . j) = ( 0. K)

 proof

 defpred P[ Nat] means 1 <= $1 & $1 < i implies (f . $1) = ( 0. K);

 let j be Nat;

 assume

 A9: 1 <= j & j < i;



 A10: for k be Nat st P[k] holds P[(k + 1)]

 proof

 let k be Nat;

 assume

 A11: P[k];

 per cases ;

 suppose

 A12: not (1 <= k & k < i);

 now

 per cases by A12;

 suppose

 A13: 1 > k;



 A14: 1 <= (1 + k) by NAT_1: 12;

 1 >= (k + 1) by A13, NAT_1: 13;

 then

 A15: (k + 1) = 1 by A14, XXREAL_0: 1;

 now

 per cases ;

 suppose (k + 1) < i;

 then (k + 1) < ( len x) by A2, XXREAL_0: 2;

 hence thesis by A4, A5, A15;

 end;

 suppose (k + 1) >= i;

 hence thesis;

 end;

 end;

 hence thesis;

 end;

 suppose k >= i;

 hence thesis by NAT_1: 12;

 end;

 end;

 hence thesis;

 end;

 suppose

 A16: 1 <= k & k < i;

 then

 A17: (k + 1) <= i by NAT_1: 13;



 A18: k < ( len x) by A2, A16, XXREAL_0: 2;

 now

 per cases by A17, XXREAL_0: 1;

 suppose

 A19: (k + 1) < i;

 then

 A20: (k + 1) < ( len x) by A2, XXREAL_0: 2;

 (f . (k + 1)) = (the addF of K . ((f . k),(x . (k + 1)))) by A6, A16, A18

 .= (( 0. K) + ( 0. K)) by A4, A11, A16, A19, A20, NAT_1: 12

 .= ( 0. K) by RLVECT_1: 4;

 hence thesis;

 end;

 suppose (k + 1) = i;

 hence thesis;

 end;

 end;

 hence thesis;

 end;

 end;



 A21: P[ 0 ];

 for l be Nat holds P[l] from NAT_1:sch 2( A21, A10);

 hence thesis by A9;

 end;

 for j st i <= j & j <= ( len x) holds (f . j) = a

 proof

 defpred P[ Nat] means i <= $1 & $1 <= ( len x) implies (f . $1) = a;

 let j;

 assume

 A22: i <= j & j <= ( len x);



 A23: for k be Nat st P[k] holds P[(k + 1)]

 proof

 let k be Nat;

 assume

 A24: P[k];

 per cases ;

 suppose not (i <= (k + 1) & (k + 1) <= ( len x));

 hence thesis;

 end;

 suppose

 A25: i <= (k + 1) & (k + 1) <= ( len x);

 then

 A26: k < ( len x) by NAT_1: 13;



 A27: 1 <= (k + 1) by A1, A25, XXREAL_0: 2;

 now

 per cases by A25, XXREAL_0: 1;

 suppose

 A28: i < (k + 1);



 A29: k < ( len x) by A25, NAT_1: 13;

 i <= k by A28, NAT_1: 13;



 then (f . (k + 1)) = (the addF of K . ((f . k),(x . (k + 1)))) by A1, A6, A29

 .= (a + ( 0. K)) by A4, A24, A25, A27, A28, NAT_1: 13

 .= a by RLVECT_1: 4;

 hence thesis;

 end;

 suppose

 A30: i = (k + 1);

 then

 A31: k < i by NAT_1: 13;

 now

 per cases ;

 suppose

 A32: 1 <= k;



 then (f . (k + 1)) = (the addF of K . ((f . k),(x . (k + 1)))) by A6, A26

 .= (( 0. K) + a) by A3, A8, A30, A31, A32

 .= a by RLVECT_1: 4;

 hence thesis;

 end;

 suppose k < 1;

 then

 A33: (k + 1) <= 1 by NAT_1: 13;

 1 <= (1 + k) by NAT_1: 12;

 then i = 1 by A30, A33, XXREAL_0: 1;

 hence thesis by A3, A5, A33, XXREAL_0: 1;

 end;

 end;

 hence thesis;

 end;

 end;

 hence thesis;

 end;

 end;



 A34: P[ 0 ] by A1;

 for l be Nat holds P[l] from NAT_1:sch 2( A34, A23);

 hence thesis by A22;

 end;

 then (f . ( len x)) = a by A2;

 hence thesis by A7, FVSUM_1:def 8;

 end;

 theorem :: MATRIX14:33

 for f1,f2 be FinSequence of K holds ( dom ( mlt (f1,f2))) = (( dom f1) /\ ( dom f2)) & for i st i in ( dom ( mlt (f1,f2))) holds (( mlt (f1,f2)) . i) = ((f1 /. i) * (f2 /. i))

 proof

 let f1,f2 be FinSequence of K;



 A1: ( rng f2) c= the carrier of K by FINSEQ_1:def 4;

 ( dom the multF of K) = [:the carrier of K, the carrier of K:] & ( rng f1) c= the carrier of K by FINSEQ_1:def 4, FUNCT_2:def 1;

 then ( mlt (f1,f2)) = (the multF of K .: (f1,f2)) & [:( rng f1), ( rng f2):] c= ( dom the multF of K) by A1, FVSUM_1:def 7, ZFMISC_1: 96;

 hence ( dom ( mlt (f1,f2))) = (( dom f1) /\ ( dom f2)) by FUNCOP_1: 69;

 thus thesis by Th4;

 end;

 theorem :: MATRIX14:34



 Th34: for x,y be FinSequence of K, i st ( len x) = m & y = ( mlt (x,( Base_FinSeq (K,m,i)))) & 1 <= i & i <= m holds (y . i) = (x . i) & for j st j <> i & 1 <= j & j <= m holds (y . j) = ( 0. K)

 proof

 let x,y be FinSequence of K, i;

 assume that

 A1: ( len x) = m and

 A2: y = ( mlt (x,( Base_FinSeq (K,m,i)))) and

 A3: 1 <= i and

 A4: i <= m;



 A5: i in ( dom x) by A1, A3, A4, FINSEQ_3: 25;

 i <= ( len ( Base_FinSeq (K,m,i))) by A4, Th23;

 then

 A6: (( Base_FinSeq (K,m,i)) /. i) = (( Base_FinSeq (K,m,i)) . i) by A3, FINSEQ_4: 15;



 A7: ( rng ( Base_FinSeq (K,m,i))) c= the carrier of K by FINSEQ_1:def 4;



 A8: ( len ( Base_FinSeq (K,m,i))) = m by Th23;

 ( dom the multF of K) = [:the carrier of K, the carrier of K:] & ( rng x) c= the carrier of K by FINSEQ_1:def 4, FUNCT_2:def 1;

 then [:( rng x), ( rng ( Base_FinSeq (K,m,i))):] c= ( dom the multF of K) by A7, ZFMISC_1: 96;

 then ( dom (the multF of K .: (x,( Base_FinSeq (K,m,i))))) = (( dom x) /\ ( dom ( Base_FinSeq (K,m,i)))) by FUNCOP_1: 69;



 then

 A9: ( dom ( mlt (x,( Base_FinSeq (K,m,i))))) = (( dom x) /\ ( dom ( Base_FinSeq (K,m,i)))) by FVSUM_1:def 7

 .= (( Seg m) /\ ( dom ( Base_FinSeq (K,m,i)))) by A1, FINSEQ_1:def 3

 .= (( Seg m) /\ ( Seg m)) by A8, FINSEQ_1:def 3

 .= ( Seg m);

 then i in ( dom ( mlt (x,( Base_FinSeq (K,m,i))))) by A3, A4, FINSEQ_1: 1;



 then (( mlt (x,( Base_FinSeq (K,m,i)))) . i) = ((x /. i) * (( Base_FinSeq (K,m,i)) /. i)) by Th4

 .= ((x /. i) * ( 1. K)) by A3, A4, A6, Th24

 .= (x /. i)

 .= (x . i) by A5, PARTFUN1:def 6;

 hence (y . i) = (x . i) by A2;

 let j;

 assume that

 A10: j <> i and

 A11: 1 <= j and

 A12: j <= m;

 j <= ( len ( Base_FinSeq (K,m,i))) by A12, Th23;



 then

 A13: (( Base_FinSeq (K,m,i)) /. j) = (( Base_FinSeq (K,m,i)) . j) by A11, FINSEQ_4: 15

 .= ( 0. K) by A10, A11, A12, Th25;

 j in ( dom ( mlt (x,( Base_FinSeq (K,m,i))))) by A9, A11, A12, FINSEQ_1: 1;



 then (( mlt (x,( Base_FinSeq (K,m,i)))) . j) = ((x /. j) * (( Base_FinSeq (K,m,i)) /. j)) by Th4

 .= ( 0. K) by A13;

 hence thesis by A2;

 end;

 theorem :: MATRIX14:35



 Th35: for x be FinSequence of K st ( len x) = m & 1 <= i & i <= m holds |(x, ( Base_FinSeq (K,m,i)))| = (x . i) & |(x, ( Base_FinSeq (K,m,i)))| = (x /. i)

 proof

 let x be FinSequence of K;

 assume that

 A1: ( len x) = m and

 A2: 1 <= i & i <= m;



 A3: for j st j <> i & 1 <= j & j <= m holds (( mlt (x,( Base_FinSeq (K,m,i)))) . j) = ( 0. K) by A1, A2, Th34;



 A4: ( len ( Base_FinSeq (K,m,i))) = m by Th23;



 A5: ( rng ( Base_FinSeq (K,m,i))) c= the carrier of K by FINSEQ_1:def 4;

 ( dom the multF of K) = [:the carrier of K, the carrier of K:] & ( rng x) c= the carrier of K by FINSEQ_1:def 4, FUNCT_2:def 1;

 then [:( rng x), ( rng ( Base_FinSeq (K,m,i))):] c= ( dom the multF of K) by A5, ZFMISC_1: 96;

 then ( dom (the multF of K .: (x,( Base_FinSeq (K,m,i))))) = (( dom x) /\ ( dom ( Base_FinSeq (K,m,i)))) by FUNCOP_1: 69;



 then ( dom ( mlt (x,( Base_FinSeq (K,m,i))))) = (( dom x) /\ ( dom ( Base_FinSeq (K,m,i)))) by FVSUM_1:def 7

 .= (( Seg m) /\ ( dom ( Base_FinSeq (K,m,i)))) by A1, FINSEQ_1:def 3

 .= (( Seg m) /\ ( Seg m)) by A4, FINSEQ_1:def 3

 .= ( Seg m);

 then

 A6: ( len ( mlt (x,( Base_FinSeq (K,m,i))))) = m by FINSEQ_1:def 3;



 A7: (x /. i) = (x . i) by A1, A2, FINSEQ_4: 15;

 then (( mlt (x,( Base_FinSeq (K,m,i)))) . i) = (x /. i) by A1, A2, Th34;

 then

 A8: ( Sum ( mlt (x,( Base_FinSeq (K,m,i))))) = (x . i) by A2, A7, A6, A3, Th32;

 hence |(x, ( Base_FinSeq (K,m,i)))| = (x . i) by FVSUM_1:def 9;

 (x . i) = (x /. i) by A1, A2, FINSEQ_4: 15;

 hence thesis by A8, FVSUM_1:def 9;

 end;

 theorem :: MATRIX14:36



 Th36: for m, i st 1 <= i & i <= m holds |(( Base_FinSeq (K,m,i)), ( Base_FinSeq (K,m,i)))| = ( 1. K)

 proof

 let m, i;

 assume

 A1: 1 <= i & i <= m;

 ( len ( Base_FinSeq (K,m,i))) = m by Th23;



 hence |(( Base_FinSeq (K,m,i)), ( Base_FinSeq (K,m,i)))| = (( Base_FinSeq (K,m,i)) . i) by A1, Th35

 .= ( 1. K) by A1, Th24;

 end;

 theorem :: MATRIX14:37



 Th37: for a be Element of K, P,Q be Matrix of n, K st n > 0 & a <> ( 0. K) & (P * (1,1)) = (a " ) & (for i st 1 < i & i <= n holds (P . i) = ( Base_FinSeq (K,n,i))) & (Q * (1,1)) = a & (for j st 1 < j & j <= n holds (Q * (1,j)) = ( - (a * (P * (1,j))))) & (for i st 1 0 and

 A2: a <> ( 0. K) and

 A3: (P * (1,1)) = (a " ) and

 A4: for i st 1 < i & i <= n holds (P . i) = ( Base_FinSeq (K,n,i)) and

 A5: (Q * (1,1)) = a and

 A6: for j st 1 < j & j <= n holds (Q * (1,j)) = ( - (a * (P * (1,j)))) and

 A7: for i st 1 < i & i <= n holds (Q . i) = ( Base_FinSeq (K,n,i));



 A8: ( 0 + 1) <= n by A1, NAT_1: 13;



 A9: ( len ( Base_FinSeq (K,n,1))) = n by Th23;



 A10: ( len P) = n by MATRIX_0: 24;



 A11: ( len ((a " ) * ( Base_FinSeq (K,n,1)))) = ( len ( Base_FinSeq (K,n,1))) by MATRIXR1: 16

 .= n by Th23;



 A12: for k be Nat st 1 <= k & k <= n holds (( Col (P,1)) . k) = (((a " ) * ( Base_FinSeq (K,n,1))) . k)

 proof

 let k be Nat;



 A13: k in NAT by ORDINAL1:def 12;

 assume that

 A14: 1 <= k and

 A15: k <= n;



 A16: k in ( Seg n) by A14, A15, FINSEQ_1: 1;

 then

 A17: k in ( dom P) by A10, FINSEQ_1:def 3;

 A18:

 now

 [k, 1] in ( Indices P) by A8, A14, A15, MATRIX_0: 31;

 then

 A19: ex p be FinSequence of K st p = (P . k) & (P * (k,1)) = (p . 1) by MATRIX_0:def 5;

 assume

 A20: k <> 1;

 then 1 < k by A14, XXREAL_0: 1;



 then (P * (k,1)) = (( Base_FinSeq (K,n,k)) . 1) by A4, A13, A15, A19

 .= ( 0. K) by A8, A20, Th25;

 hence (( Col (P,1)) . k) = ( 0. K) by A17, MATRIX_0:def 8;

 end;



 A21: (( Base_FinSeq (K,n,1)) /. k) = (( Base_FinSeq (K,n,1)) . k) by A9, A14, A15, FINSEQ_4: 15;

 A22:

 now

 assume

 A23: k = 1;

 k in ( dom ((a " ) * ( Base_FinSeq (K,n,1)))) by A11, A16, FINSEQ_1:def 3;



 hence (((a " ) * ( Base_FinSeq (K,n,1))) . k) = ((a " ) * (( Base_FinSeq (K,n,1)) /. k)) by A21, FVSUM_1: 50

 .= ((a " ) * ( 1. K)) by A15, A21, A23, Th24

 .= (a " );

 end;



 A24: k in ( dom ((a " ) * ( Base_FinSeq (K,n,1)))) by A11, A14, A15, FINSEQ_3: 25;

 A25:

 now

 assume

 A26: k <> 1;



 thus (((a " ) * ( Base_FinSeq (K,n,1))) . k) = ((a " ) * (( Base_FinSeq (K,n,1)) /. k)) by A24, A21, FVSUM_1: 50

 .= ((a " ) * ( 0. K)) by A14, A15, A21, A26, Th25

 .= ( 0. K);

 end;

 1 <= n by A14, A15, XXREAL_0: 2;

 then 1 in ( dom P) by A10, FINSEQ_3: 25;

 hence thesis by A3, A25, A22, A18, MATRIX_0:def 8;

 end;



 A27: ( 0 + 1) <= n by A1, NAT_1: 13;



 A28: ( len Q) = n by MATRIX_0: 24;

 then

 A29: 1 in ( Seg ( len Q)) by A27, FINSEQ_1: 1;

 then

 A30: 1 in ( dom Q) by FINSEQ_1:def 3;



 A31: ( width Q) = n by MATRIX_0: 24;

 then

 A32: ( len ( Line (Q,1))) = n by MATRIX_0:def 7;

 then

 A33: 1 in ( dom ( Line (Q,1))) by A28, A29, FINSEQ_1:def 3;



 A34: for j st 1 < j & j <= n holds (P * (1,j)) = ( - ((a " ) * (Q * (1,j))))

 proof

 let j;

 assume 1 < j & j <= n;

 then ( - ((a " ) * (Q * (1,j)))) = ( - ((a " ) * ( - (a * (P * (1,j)))))) by A6;

 then ( - ((a " ) * (Q * (1,j)))) = ( - ((a " ) * (( - a) * (P * (1,j))))) by VECTSP_1: 9;

 then ( - ((a " ) * (Q * (1,j)))) = (( - (a " )) * (( - a) * (P * (1,j)))) by VECTSP_1: 9;

 then ( - ((a " ) * (Q * (1,j)))) = ((( - (a " )) * ( - a)) * (P * (1,j))) by GROUP_1:def 3;

 then ( - ((a " ) * (Q * (1,j)))) = ((a * (a " )) * (P * (1,j))) by VECTSP_1: 10;

 then ( - ((a " ) * (Q * (1,j)))) = (( 1. K) * (P * (1,j))) by A2, VECTSP_1:def 10;

 hence thesis;

 end;



 A35: for j st 1 < j & j <= n holds ((Q * P) * (1,j)) = ( 0. K)

 proof

 let j;

 assume that

 A36: 1 < j and

 A37: j <= n;



 A38: ( len ( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1))))) = ( len (( - ((a " ) * (Q * (1,j)))) * ( Base_FinSeq (K,n,1)))) by Th6

 .= ( len ( Base_FinSeq (K,n,1))) by MATRIXR1: 16

 .= n by Th23;



 A39: j in ( Seg n) by A36, A37, FINSEQ_1: 1;



 A40: 1 <= n by A36, A37, XXREAL_0: 2;

 then

 A41: 1 in ( Seg ( width Q)) by A31, FINSEQ_1: 1;

 ( len ( Line (Q,1))) = n by A31, MATRIX_0:def 7;

 then

 A42: (( Line (Q,1)) /. j) = (( Line (Q,1)) . j) by A36, A37, FINSEQ_4: 15;



 A43: (( Line (Q,1)) /. 1) = (( Line (Q,1)) . 1) by A32, A40, FINSEQ_4: 15

 .= a by A5, A41, MATRIX_0:def 7;



 A44: ( len ( Col (P,j))) = ( len P) by MATRIX_0:def 8

 .= n by MATRIX_0: 24;

 reconsider p = ( Col (P,j)), q = (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) + ( Base_FinSeq (K,n,j))) as FinSequence of K;



 A45: ( len ( Base_FinSeq (K,n,j))) = n by Th23;



 A46: ( len (( - ((a " ) * (Q * (1,j)))) * ( Base_FinSeq (K,n,1)))) = ( len ( Base_FinSeq (K,n,1))) by MATRIXR1: 16

 .= n by Th23;



 A47: for k be Nat st 1 <= k & k <= n holds (p . k) = (q . k)

 proof



 A48: ( len (( - ((a " ) * (Q * (1,j)))) * ( Base_FinSeq (K,n,1)))) = ( len ( Base_FinSeq (K,n,1))) by MATRIXR1: 16

 .= n by Th23;

 let k be Nat;

 assume that

 A49: 1 <= k and

 A50: k <= n;



 A51: k in ( dom (( - ((a " ) * (Q * (1,j)))) * ( Base_FinSeq (K,n,1)))) by A46, A49, A50, FINSEQ_3: 25;

 ( len ( Base_FinSeq (K,n,1))) = n by Th23;

 then

 A52: (( Base_FinSeq (K,n,1)) /. k) = (( Base_FinSeq (K,n,1)) . k) by A49, A50, FINSEQ_4: 15;

 k in ( dom P) by A10, A49, A50, FINSEQ_3: 25;

 then

 A53: (p . k) = (P * (k,j)) by MATRIX_0:def 8;



 A54: (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) = ((( - ((a " ) * (Q * (1,j)))) * ( Base_FinSeq (K,n,1))) . k) by Th6

 .= (( - ((a " ) * (Q * (1,j)))) * (( Base_FinSeq (K,n,1)) /. k)) by A51, A52, FVSUM_1: 50;

 per cases by A49, XXREAL_0: 1;

 suppose

 A55: 1 = k;

 then 1 <= ( len ( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1))))) by A50, A48, Th6;



 then

 A56: (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) /. 1) = (( - ((a " ) * (Q * (1,j)))) * (( Base_FinSeq (K,n,1)) /. 1)) by A54, A55, FINSEQ_4: 15

 .= (( - ((a " ) * (Q * (1,j)))) * ( 1. K)) by A27, A52, A55, Th24

 .= ( - ((a " ) * (Q * (1,j))));



 A57: (p . 1) = ( - ((a " ) * (Q * (1,j)))) by A34, A36, A37, A53, A55;

 (( Base_FinSeq (K,n,j)) /. 1) = (( Base_FinSeq (K,n,j)) . 1) by A45, A50, A55, FINSEQ_4: 15

 .= ( 0. K) by A36, A50, A55, Th25;

 then (q . 1) = (( - ((a " ) * (Q * (1,j)))) + ( 0. K)) by A38, A45, A50, A55, A56, Th5;

 hence thesis by A55, A57, RLVECT_1: 4;

 end;

 suppose

 A58: 1 < k;

 [k, j] in ( Indices P) by A36, A37, A49, A50, MATRIX_0: 31;

 then

 A59: ex p2 be FinSequence of K st p2 = (P . k) & (P * (k,j)) = (p2 . j) by MATRIX_0:def 5;

 k in NAT by ORDINAL1:def 12;

 then

 A60: (p . k) = (( Base_FinSeq (K,n,k)) . j) by A4, A50, A53, A58, A59;

 now

 per cases ;

 suppose

 A61: k <> j;

 ( len ( Base_FinSeq (K,n,1))) = n by Th23;

 then (( Base_FinSeq (K,n,1)) /. k) = (( Base_FinSeq (K,n,1)) . k) by A49, A50, FINSEQ_4: 15;



 then

 A62: (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) = (( - ((a " ) * (Q * (1,j)))) * ( 0. K)) by A50, A54, A58, Th25

 .= ( 0. K);



 A63: (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) /. k) = (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) by A38, A49, A50, FINSEQ_4: 15;



 A64: (p . k) = ( 0. K) by A36, A37, A60, A61, Th25;

 (( Base_FinSeq (K,n,j)) /. k) = (( Base_FinSeq (K,n,j)) . k) by A45, A49, A50, FINSEQ_4: 15

 .= ( 0. K) by A49, A50, A61, Th25;

 then (q . k) = (( 0. K) + ( 0. K)) by A38, A45, A49, A50, A63, A62, Th5;

 hence thesis by A64, RLVECT_1: 4;

 end;

 suppose

 A65: k = j;

 then

 A66: (p . k) = ( 1. K) by A49, A50, A60, Th24;



 A67: (( - (((a " ) * (Q * (1,k))) * ( Base_FinSeq (K,n,1)))) /. k) = (( - (((a " ) * (Q * (1,k))) * ( Base_FinSeq (K,n,1)))) . k) by A38, A49, A50, A65, FINSEQ_4: 15;

 ( len ( Base_FinSeq (K,n,1))) = n by Th23;

 then (( Base_FinSeq (K,n,1)) /. k) = (( Base_FinSeq (K,n,1)) . k) by A49, A50, FINSEQ_4: 15;



 then

 A68: (( - (((a " ) * (Q * (1,k))) * ( Base_FinSeq (K,n,1)))) . k) = (( - ((a " ) * (Q * (1,k)))) * ( 0. K)) by A50, A54, A58, A65, Th25

 .= ( 0. K);

 (( Base_FinSeq (K,n,k)) /. k) = (( Base_FinSeq (K,n,k)) . k) by A45, A49, A50, A65, FINSEQ_4: 15

 .= ( 1. K) by A36, A37, A65, Th24;

 then (q . k) = (( 0. K) + ( 1. K)) by A38, A45, A49, A50, A65, A67, A68, Th5;

 hence thesis by A66, RLVECT_1: 4;

 end;

 end;

 hence thesis;

 end;

 end;

 ( len (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) + ( Base_FinSeq (K,n,j)))) = n by A38, A45, Th2;

 then

 A69: ( Col (P,j)) = (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) + ( Base_FinSeq (K,n,j))) by A44, A47, FINSEQ_1: 14;

 [1, j] in ( Indices (Q * P)) by A27, A36, A37, MATRIX_0: 31;



 then ((Q * P) * (1,j)) = |(( Line (Q,1)), ( Col (P,j)))| by A10, A31, MATRIX_3:def 4

 .= ( |(( Line (Q,1)), ( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))))| + |(( Line (Q,1)), ( Base_FinSeq (K,n,j)))|) by A32, A38, A45, A69, Th11

 .= ( |(( Line (Q,1)), (( - ((a " ) * (Q * (1,j)))) * ( Base_FinSeq (K,n,1))))| + |(( Line (Q,1)), ( Base_FinSeq (K,n,j)))|) by Th6

 .= ((( - ((a " ) * (Q * (1,j)))) * |(( Line (Q,1)), ( Base_FinSeq (K,n,1)))|) + |(( Line (Q,1)), ( Base_FinSeq (K,n,j)))|) by A32, A9, Th10

 .= ((( - ((a " ) * (Q * (1,j)))) * a) + |(( Line (Q,1)), ( Base_FinSeq (K,n,j)))|) by A32, A27, A43, Th35

 .= (( - (((a " ) * (Q * (1,j))) * a)) + |(( Line (Q,1)), ( Base_FinSeq (K,n,j)))|) by VECTSP_1: 9

 .= (( - ((Q * (1,j)) * ((a " ) * a))) + |(( Line (Q,1)), ( Base_FinSeq (K,n,j)))|) by GROUP_1:def 3

 .= (( - ((Q * (1,j)) * ( 1. K))) + |(( Line (Q,1)), ( Base_FinSeq (K,n,j)))|) by A2, VECTSP_1:def 10

 .= (( - ((Q * (1,j)) * ( 1. K))) + (( Line (Q,1)) /. j)) by A32, A36, A37, Th35

 .= (( - (Q * (1,j))) + (( Line (Q,1)) /. j))

 .= (( - (Q * (1,j))) + (Q * (1,j))) by A31, A39, A42, MATRIX_0:def 7

 .= ( 0. K) by RLVECT_1: 5;

 hence thesis;

 end;



 A70: 1 in ( Seg ( width Q)) by A31, A27, FINSEQ_1: 1;



 A71: for i, j st 1 < i & i <= n & i = j holds ((Q * P) * (i,j)) = ( 1. K)

 proof

 let i, j;

 assume that

 A72: 1 < i and

 A73: i <= n and

 A74: i = j;



 A75: ( len ( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1))))) = ( len (( - ((a " ) * (Q * (1,j)))) * ( Base_FinSeq (K,n,1)))) by Th6

 .= ( len ( Base_FinSeq (K,n,1))) by MATRIXR1: 16

 .= n by Th23;

 [i, j] in ( Indices Q) by A72, A73, A74, MATRIX_0: 31;

 then

 consider p1 be FinSequence of K such that

 A76: p1 = (Q . i) and

 A77: (Q * (i,j)) = (p1 . j) by MATRIX_0:def 5;

 p1 = ( Base_FinSeq (K,n,i)) by A7, A72, A73, A76;

 then

 A78: (p1 . j) = ( 1. K) by A72, A73, A74, Th24;

 [i, 1] in ( Indices Q) by A8, A72, A73, MATRIX_0: 31;

 then

 consider p2 be FinSequence of K such that

 A79: p2 = (Q . i) and

 A80: (Q * (i,1)) = (p2 . 1) by MATRIX_0:def 5;



 A81: ( width Q) = n by MATRIX_0: 24;



 A82: j in ( Seg n) by A72, A73, A74, FINSEQ_1: 1;



 A83: ( len ( Col (P,j))) = ( len P) by MATRIX_0:def 8

 .= n by MATRIX_0: 24;

 reconsider p = ( Col (P,j)), q = (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) + ( Base_FinSeq (K,n,j))) as FinSequence of K;



 A84: ( len ( Base_FinSeq (K,n,j))) = n by Th23;



 A85: ( len (( - ((a " ) * (Q * (1,j)))) * ( Base_FinSeq (K,n,1)))) = ( len ( Base_FinSeq (K,n,1))) by MATRIXR1: 16

 .= n by Th23;



 A86: for k be Nat st 1 <= k & k <= n holds (p . k) = (q . k)

 proof



 A87: ( len (( - ((a " ) * (Q * (1,j)))) * ( Base_FinSeq (K,n,1)))) = ( len ( Base_FinSeq (K,n,1))) by MATRIXR1: 16

 .= n by Th23;

 let k be Nat;

 assume that

 A88: 1 <= k and

 A89: k <= n;

 k in ( Seg n) by A88, A89, FINSEQ_1: 1;

 then

 A90: k in ( dom (( - ((a " ) * (Q * (1,j)))) * ( Base_FinSeq (K,n,1)))) by A85, FINSEQ_1:def 3;

 ( len ( Base_FinSeq (K,n,1))) = n by Th23;

 then

 A91: (( Base_FinSeq (K,n,1)) /. k) = (( Base_FinSeq (K,n,1)) . k) by A88, A89, FINSEQ_4: 15;

 k in ( dom P) by A10, A88, A89, FINSEQ_3: 25;

 then

 A92: (p . k) = (P * (k,j)) by MATRIX_0:def 8;



 A93: (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) = ((( - ((a " ) * (Q * (1,j)))) * ( Base_FinSeq (K,n,1))) . k) by Th6

 .= (( - ((a " ) * (Q * (1,j)))) * (( Base_FinSeq (K,n,1)) /. k)) by A90, A91, FVSUM_1: 50;

 per cases by A88, XXREAL_0: 1;

 suppose

 A94: 1 = k;

 k <= ( len ( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1))))) by A89, A87, Th6;



 then

 A95: (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) /. k) = (( - ((a " ) * (Q * (1,j)))) * (( Base_FinSeq (K,n,1)) /. k)) by A88, A93, FINSEQ_4: 15

 .= (( - ((a " ) * (Q * (1,j)))) * ( 1. K)) by A27, A91, A94, Th24

 .= ( - ((a " ) * (Q * (1,j))));

 (( Base_FinSeq (K,n,j)) /. k) = (( Base_FinSeq (K,n,j)) . k) by A84, A88, A89, FINSEQ_4: 15

 .= ( 0. K) by A72, A74, A89, A94, Th25;

 then

 A96: (q . k) = (( - ((a " ) * (Q * (1,j)))) + ( 0. K)) by A75, A84, A88, A89, A95, Th5;

 (p . k) = ( - ((a " ) * (Q * (1,j)))) by A34, A72, A73, A74, A92, A94;

 hence thesis by A96, RLVECT_1: 4;

 end;

 suppose

 A97: 1 < k;

 [k, j] in ( Indices P) by A72, A73, A74, A88, A89, MATRIX_0: 31;

 then

 A98: ex p2 be FinSequence of K st p2 = (P . k) & (P * (k,j)) = (p2 . j) by MATRIX_0:def 5;

 k in NAT by ORDINAL1:def 12;

 then

 A99: (p . k) = (( Base_FinSeq (K,n,k)) . j) by A4, A89, A92, A97, A98;

 now

 per cases ;

 suppose

 A100: k <> j;

 ( len ( Base_FinSeq (K,n,1))) = n by Th23;

 then (( Base_FinSeq (K,n,1)) /. k) = (( Base_FinSeq (K,n,1)) . k) by A88, A89, FINSEQ_4: 15;



 then

 A101: (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) = (( - ((a " ) * (Q * (1,j)))) * ( 0. K)) by A89, A93, A97, Th25

 .= ( 0. K);



 A102: (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) /. k) = (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) by A75, A88, A89, FINSEQ_4: 15;



 A103: (p . k) = ( 0. K) by A72, A73, A74, A99, A100, Th25;

 (( Base_FinSeq (K,n,j)) /. k) = (( Base_FinSeq (K,n,j)) . k) by A84, A88, A89, FINSEQ_4: 15

 .= ( 0. K) by A88, A89, A100, Th25;

 then (q . k) = (( 0. K) + ( 0. K)) by A75, A84, A88, A89, A102, A101, Th5;

 hence thesis by A103, RLVECT_1: 4;

 end;

 suppose

 A104: k = j;

 ( len ( Base_FinSeq (K,n,1))) = n by Th23;

 then (( Base_FinSeq (K,n,1)) /. k) = (( Base_FinSeq (K,n,1)) . k) by A88, A89, FINSEQ_4: 15;



 then

 A105: (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) = (( - ((a " ) * (Q * (1,j)))) * ( 0. K)) by A89, A93, A97, Th25

 .= ( 0. K);



 A106: (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) /. k) = (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) by A75, A88, A89, FINSEQ_4: 15;



 A107: (p . k) = ( 1. K) by A88, A89, A99, A104, Th24;

 (( Base_FinSeq (K,n,j)) /. k) = (( Base_FinSeq (K,n,j)) . k) by A84, A88, A89, FINSEQ_4: 15

 .= ( 1. K) by A88, A89, A104, Th24;

 then (q . k) = (( 0. K) + ( 1. K)) by A75, A84, A88, A89, A106, A105, Th5;

 hence thesis by A107, RLVECT_1: 4;

 end;

 end;

 hence thesis;

 end;

 end;

 ( len (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) + ( Base_FinSeq (K,n,j)))) = n by A75, A84, Th2;

 then

 A108: ( Col (P,j)) = (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) + ( Base_FinSeq (K,n,j))) by A83, A86, FINSEQ_1: 14;



 A109: ( len ( Line (Q,i))) = n by A31, MATRIX_0:def 7;



 then

 A110: (( Line (Q,i)) /. 1) = (( Line (Q,i)) . 1) by A27, FINSEQ_4: 15

 .= (Q * (i,1)) by A70, MATRIX_0:def 7;



 A111: (( Line (Q,i)) /. j) = (( Line (Q,i)) . j) by A72, A73, A74, A109, FINSEQ_4: 15

 .= (Q * (i,j)) by A82, A81, MATRIX_0:def 7;

 [i, j] in ( Indices (Q * P)) by A72, A73, A74, MATRIX_0: 31;



 then

 A112: ((Q * P) * (i,j)) = |(( Line (Q,i)), ( Col (P,j)))| by A10, A81, MATRIX_3:def 4

 .= ( |(( Line (Q,i)), ( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))))| + |(( Line (Q,i)), ( Base_FinSeq (K,n,j)))|) by A75, A84, A108, A109, Th11

 .= ( |(( Line (Q,i)), (( - ((a " ) * (Q * (1,j)))) * ( Base_FinSeq (K,n,1))))| + |(( Line (Q,i)), ( Base_FinSeq (K,n,j)))|) by Th6

 .= ((( - ((a " ) * (Q * (1,j)))) * |(( Line (Q,i)), ( Base_FinSeq (K,n,1)))|) + |(( Line (Q,i)), ( Base_FinSeq (K,n,j)))|) by A9, A109, Th10

 .= ((( - ((a " ) * (Q * (1,j)))) * (Q * (i,1))) + |(( Line (Q,i)), ( Base_FinSeq (K,n,j)))|) by A27, A109, A110, Th35

 .= (( - (((Q * (1,j)) * (a " )) * (Q * (i,1)))) + |(( Line (Q,i)), ( Base_FinSeq (K,n,j)))|) by VECTSP_1: 9

 .= (( - ((Q * (1,j)) * ((a " ) * (Q * (i,1))))) + |(( Line (Q,i)), ( Base_FinSeq (K,n,j)))|) by GROUP_1:def 3

 .= (( - ((Q * (1,j)) * ((a " ) * (Q * (i,1))))) + (Q * (i,j))) by A72, A73, A74, A109, A111, Th35;



 A113: 1 <= n by A72, A73, XXREAL_0: 2;

 p2 = ( Base_FinSeq (K,n,i)) by A7, A72, A73, A79;



 hence ((Q * P) * (i,j)) = (( - ((Q * (1,j)) * ((a " ) * ( 0. K)))) + (Q * (i,j))) by A72, A113, A112, A80, Th25

 .= (( - ((Q * (1,j)) * ( 0. K))) + (Q * (i,j)))

 .= (( - ( 0. K)) + (Q * (i,j)))

 .= (( 0. K) + ( 1. K)) by A77, A78, RLVECT_1: 12

 .= ( 1. K) by RLVECT_1: 4;

 end;



 A114: ( Indices P) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;



 A115: for i, j st 1 j holds ((Q * P) * (i,j)) = ( 0. K)

 proof



 A116: ( len ((a " ) * ( Base_FinSeq (K,n,1)))) = ( len ( Base_FinSeq (K,n,1))) by MATRIXR1: 16

 .= n by Th23;

 let i, j;

 assume that

 A117: 1 j;



 A122: [i, j] in ( Indices (Q * P)) by A117, A118, A119, A120, MATRIX_0: 31;



 A123: j in ( Seg n) by A119, A120, FINSEQ_1: 1;



 A124: ( len (( - ((a " ) * (Q * (1,j)))) * ( Base_FinSeq (K,n,1)))) = ( len ( Base_FinSeq (K,n,1))) by MATRIXR1: 16

 .= n by Th23;



 A125: ( len ( Col (P,j))) = ( len P) by MATRIX_0:def 8

 .= n by MATRIX_0: 24;



 A126: [i, 1] in ( Indices Q) by A27, A117, A118, MATRIX_0: 31;



 A127: ( len ( Base_FinSeq (K,n,j))) = n by Th23;



 A128: ( len ( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1))))) = ( len (( - ((a " ) * (Q * (1,j)))) * ( Base_FinSeq (K,n,1)))) by Th6

 .= ( len ( Base_FinSeq (K,n,1))) by MATRIXR1: 16

 .= n by Th23;

 then

 A129: ( len (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) + ( Base_FinSeq (K,n,j)))) = n by A127, Th2;



 A130: [i, j] in ( Indices Q) by A117, A118, A119, A120, MATRIX_0: 31;

 now

 per cases ;

 suppose

 A131: j > 1;

 reconsider p = ( Col (P,j)), q = (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) + ( Base_FinSeq (K,n,j))) as FinSequence of K;

 for k be Nat st 1 <= k & k <= n holds (p . k) = (q . k)

 proof

 let k be Nat;

 assume that

 A132: 1 <= k and

 A133: k <= n;

 k in ( Seg n) by A132, A133, FINSEQ_1: 1;

 then

 A134: k in ( dom (( - ((a " ) * (Q * (1,j)))) * ( Base_FinSeq (K,n,1)))) by A124, FINSEQ_1:def 3;

 ( len ( Base_FinSeq (K,n,1))) = n by Th23;

 then

 A135: (( Base_FinSeq (K,n,1)) /. k) = (( Base_FinSeq (K,n,1)) . k) by A132, A133, FINSEQ_4: 15;

 k in ( dom P) by A10, A132, A133, FINSEQ_3: 25;

 then

 A136: (p . k) = (P * (k,j)) by MATRIX_0:def 8;



 A137: (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) = ((( - ((a " ) * (Q * (1,j)))) * ( Base_FinSeq (K,n,1))) . k) by Th6

 .= (( - ((a " ) * (Q * (1,j)))) * (( Base_FinSeq (K,n,1)) /. k)) by A134, A135, FVSUM_1: 50;

 ( len ( Base_FinSeq (K,n,1))) = n by Th23;

 then

 A138: (( Base_FinSeq (K,n,1)) /. k) = (( Base_FinSeq (K,n,1)) . k) by A132, A133, FINSEQ_4: 15;

 per cases by A132, XXREAL_0: 1;

 suppose

 A139: 1 = k;

 then

 A140: (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) = (( - ((a " ) * (Q * (1,j)))) * ( 1. K)) by A27, A135, A137, Th24;



 A141: (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) /. k) = (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) by A128, A132, A133, FINSEQ_4: 15;

 (( Base_FinSeq (K,n,j)) /. k) = (( Base_FinSeq (K,n,j)) . k) by A127, A132, A133, FINSEQ_4: 15

 .= ( 0. K) by A131, A133, A139, Th25;



 then (q . k) = ((( - ((a " ) * (Q * (1,j)))) * ( 1. K)) + ( 0. K)) by A128, A127, A132, A133, A141, A140, Th5

 .= (( - ((a " ) * (Q * (1,j)))) * ( 1. K)) by RLVECT_1: 4

 .= ( - ((a " ) * (Q * (1,j))));

 hence thesis by A34, A120, A131, A136, A139;

 end;

 suppose

 A142: 1 < k;

 [k, j] in ( Indices P) by A119, A120, A132, A133, MATRIX_0: 31;

 then

 A143: ex p2 be FinSequence of K st p2 = (P . k) & (P * (k,j)) = (p2 . j) by MATRIX_0:def 5;

 k in NAT by ORDINAL1:def 12;

 then

 A144: (p . k) = (( Base_FinSeq (K,n,k)) . j) by A4, A133, A136, A142, A143;

 now

 per cases ;

 suppose

 A145: k <> j;

 (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) /. k) = (( - ((a " ) * (Q * (1,j)))) * (( Base_FinSeq (K,n,1)) /. k)) by A128, A132, A133, A137, FINSEQ_4: 15

 .= (( - ((a " ) * (Q * (1,j)))) * ( 0. K)) by A133, A138, A142, Th25

 .= ( 0. K);



 then (q . k) = (( 0. K) + (( Base_FinSeq (K,n,j)) /. k)) by A128, A127, A132, A133, Th5

 .= (( Base_FinSeq (K,n,j)) /. k) by RLVECT_1: 4

 .= (( Base_FinSeq (K,n,j)) . k) by A127, A132, A133, FINSEQ_4: 15

 .= ( 0. K) by A132, A133, A145, Th25;

 hence thesis by A119, A120, A144, A145, Th25;

 end;

 suppose

 A146: k = j;

 (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) /. k) = (( - ((a " ) * (Q * (1,j)))) * (( Base_FinSeq (K,n,1)) /. k)) by A128, A132, A133, A137, FINSEQ_4: 15

 .= (( - ((a " ) * (Q * (1,j)))) * ( 0. K)) by A133, A138, A142, Th25

 .= ( 0. K);



 then (q . k) = (( 0. K) + (( Base_FinSeq (K,n,j)) /. k)) by A128, A127, A132, A133, Th5

 .= (( Base_FinSeq (K,n,j)) /. k) by RLVECT_1: 4

 .= (( Base_FinSeq (K,n,j)) . k) by A127, A132, A133, FINSEQ_4: 15

 .= ( 1. K) by A119, A120, A146, Th24;

 hence thesis by A132, A133, A144, A146, Th24;

 end;

 end;

 hence thesis;

 end;

 end;

 then

 A147: ( Col (P,j)) = (( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))) + ( Base_FinSeq (K,n,j))) by A125, A129, FINSEQ_1: 14;



 A148: 1 <= n by A117, A118, XXREAL_0: 2;



 A149: ( width Q) = n by MATRIX_0: 24;

 then

 A150: ( len ( Line (Q,i))) = n by MATRIX_0:def 7;



 then

 A151: (( Line (Q,i)) /. j) = (( Line (Q,i)) . j) by A119, A120, FINSEQ_4: 15

 .= (Q * (i,j)) by A123, A149, MATRIX_0:def 7;



 A152: (( Line (Q,i)) /. 1) = (( Line (Q,i)) . 1) by A27, A150, FINSEQ_4: 15

 .= (Q * (i,1)) by A70, MATRIX_0:def 7;



 A153: ((Q * P) * (i,j)) = |(( Line (Q,i)), ( Col (P,j)))| by A10, A122, A149, MATRIX_3:def 4

 .= ( |(( Line (Q,i)), ( - (((a " ) * (Q * (1,j))) * ( Base_FinSeq (K,n,1)))))| + |(( Line (Q,i)), ( Base_FinSeq (K,n,j)))|) by A128, A127, A147, A150, Th11

 .= ( |(( Line (Q,i)), (( - ((a " ) * (Q * (1,j)))) * ( Base_FinSeq (K,n,1))))| + |(( Line (Q,i)), ( Base_FinSeq (K,n,j)))|) by Th6

 .= ((( - ((a " ) * (Q * (1,j)))) * |(( Line (Q,i)), ( Base_FinSeq (K,n,1)))|) + |(( Line (Q,i)), ( Base_FinSeq (K,n,j)))|) by A9, A150, Th10

 .= ((( - ((a " ) * (Q * (1,j)))) * (Q * (i,1))) + |(( Line (Q,i)), ( Base_FinSeq (K,n,j)))|) by A27, A150, A152, Th35

 .= (( - (((Q * (1,j)) * (a " )) * (Q * (i,1)))) + |(( Line (Q,i)), ( Base_FinSeq (K,n,j)))|) by VECTSP_1: 9

 .= (( - ((Q * (1,j)) * ((a " ) * (Q * (i,1))))) + |(( Line (Q,i)), ( Base_FinSeq (K,n,j)))|) by GROUP_1:def 3

 .= (( - ((Q * (1,j)) * ((a " ) * (Q * (i,1))))) + (Q * (i,j))) by A119, A120, A150, A151, Th35;

 consider p2 be FinSequence of K such that

 A154: p2 = (Q . i) and

 A155: (Q * (i,1)) = (p2 . 1) by A126, MATRIX_0:def 5;

 consider p1 be FinSequence of K such that

 A156: p1 = (Q . i) and

 A157: (Q * (i,j)) = (p1 . j) by A130, MATRIX_0:def 5;

 p1 = ( Base_FinSeq (K,n,i)) by A7, A117, A118, A156;

 then

 A158: (p1 . j) = ( 0. K) by A119, A120, A121, Th25;

 p2 = ( Base_FinSeq (K,n,i)) by A7, A117, A118, A154;



 hence ((Q * P) * (i,j)) = (( - ((Q * (1,j)) * ((a " ) * ( 0. K)))) + (Q * (i,j))) by A117, A148, A153, A155, Th25

 .= (( - ((Q * (1,j)) * ( 0. K))) + (Q * (i,j)))

 .= (( - ( 0. K)) + (Q * (i,j)))

 .= (( 0. K) + ( 0. K)) by A157, A158, RLVECT_1: 12

 .= ( 0. K) by RLVECT_1: 4;

 end;

 suppose

 A159: j <= 1;

 reconsider p = ( Col (P,j)), q = ((a " ) * ( Base_FinSeq (K,n,1))) as FinSequence of K;



 A160: for k be Nat st 1 <= k & k <= n holds (p . k) = (q . k)

 proof

 let k be Nat;

 assume that

 A161: 1 <= k and

 A162: k <= n;



 A163: ( len ( Base_FinSeq (K,n,1))) = n by Th23;

 then

 A164: (( Base_FinSeq (K,n,1)) /. k) = (( Base_FinSeq (K,n,1)) . k) by A161, A162, FINSEQ_4: 15;



 A165: k in ( Seg n) by A161, A162, FINSEQ_1: 1;

 then k in ( dom ((a " ) * ( Base_FinSeq (K,n,1)))) by A116, FINSEQ_1:def 3;

 then

 A166: (((a " ) * ( Base_FinSeq (K,n,1))) . k) = ((a " ) * (( Base_FinSeq (K,n,1)) /. k)) by A164, FVSUM_1: 50;

 k in ( dom P) by A10, A161, A162, FINSEQ_3: 25;

 then

 A167: (p . k) = (P * (k,j)) by MATRIX_0:def 8;

 per cases by A161, XXREAL_0: 1;

 suppose

 A168: 1 = k;



 then (q . k) = ((a " ) * ( 1. K)) by A162, A164, A166, Th24

 .= (a " );

 hence thesis by A3, A119, A159, A167, A168, XXREAL_0: 1;

 end;

 suppose

 A169: 1 < k;

 [k, j] in ( Indices P) by A114, A123, A165, ZFMISC_1: 87;

 then

 A170: ex p2 be FinSequence of K st p2 = (P . k) & (P * (k,j)) = (p2 . j) by MATRIX_0:def 5;

 k in NAT by ORDINAL1:def 12;

 then

 A171: (p . k) = (( Base_FinSeq (K,n,k)) . j) by A4, A162, A167, A169, A170;

 now

 per cases ;

 suppose

 A172: k <> j;

 (( Base_FinSeq (K,n,1)) /. k) = (( Base_FinSeq (K,n,1)) . k) by A161, A162, A163, FINSEQ_4: 15;



 then ((a " ) * (( Base_FinSeq (K,n,1)) /. k)) = ((a " ) * ( 0. K)) by A162, A169, Th25

 .= ( 0. K);

 hence thesis by A119, A120, A166, A171, A172, Th25;

 end;

 suppose k = j;

 hence thesis by A159, A169;

 end;

 end;

 hence thesis;

 end;

 end;



 A173: 1 <= n by A117, A118, XXREAL_0: 2;



 A174: ( width Q) = n by MATRIX_0: 24;

 then

 A175: ( len ( Line (Q,i))) = n by MATRIX_0:def 7;



 then

 A176: (( Line (Q,i)) /. 1) = (( Line (Q,i)) . 1) by A27, FINSEQ_4: 15

 .= (Q * (i,1)) by A70, MATRIX_0:def 7;



 A177: ((Q * P) * (i,j)) = |(( Line (Q,i)), ( Col (P,j)))| by A10, A122, A174, MATRIX_3:def 4

 .= |(( Line (Q,i)), ((a " ) * ( Base_FinSeq (K,n,1))))| by A125, A116, A160, FINSEQ_1: 14

 .= ((a " ) * |(( Line (Q,i)), ( Base_FinSeq (K,n,1)))|) by A9, A175, Th10

 .= ((a " ) * (Q * (i,1))) by A27, A175, A176, Th35;

 consider p2 be FinSequence of K such that

 A178: p2 = (Q . i) and

 A179: (Q * (i,1)) = (p2 . 1) by A126, MATRIX_0:def 5;

 p2 = ( Base_FinSeq (K,n,i)) by A7, A117, A118, A178;



 hence ((Q * P) * (i,j)) = ((a " ) * ( 0. K)) by A117, A173, A177, A179, Th25

 .= ( 0. K);

 end;

 end;

 hence thesis;

 end;

 ( len ( Col (P,1))) = ( len P) by MATRIX_0:def 8

 .= n by MATRIX_0: 24;

 then

 A180: ( Col (P,1)) = ((a " ) * ( Base_FinSeq (K,n,1))) by A11, A12, FINSEQ_1: 14;



 A181: ( Indices (Q * P)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;



 A182: ( len ((a " ) * ( Line (Q,1)))) = ( len ( Line (Q,1))) by MATRIXR1: 16

 .= n by A31, MATRIX_0:def 7;

 ( Indices Q) = [:( Seg n), ( Seg n):] & [1, 1] in ( Indices Q) by A27, MATRIX_0: 24, MATRIX_0: 31;



 then

 A183: ((Q * P) * (1,1)) = |(( Line (Q,1)), ( Col (P,1)))| by A10, A31, A181, MATRIX_3:def 4

 .= ((a " ) * |(( Line (Q,1)), ( Base_FinSeq (K,n,1)))|) by A32, A9, A180, Th10

 .= ((a " ) * (( Line (Q,1)) /. 1)) by A32, A27, Th35

 .= (((a " ) * ( Line (Q,1))) /. 1) by A33, POLYNOM1:def 1

 .= (((a " ) * ( Line (Q,1))) . 1) by A27, A182, FINSEQ_4: 15

 .= ((a " ) * (Q * (1,1))) by A70, A30, MATRIX12: 3

 .= ( 1. K) by A2, A5, VECTSP_1:def 10;

 for i,j be Nat st [i, j] in ( Indices (Q * P)) holds ((Q * P) * (i,j)) = (( 1. (K,n)) * (i,j))

 proof

 let i,j be Nat;

 reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def 12;

 assume

 A184: [i, j] in ( Indices (Q * P));

 then

 A185: i in ( Seg n) by A181, ZFMISC_1: 87;

 then

 A186: 1 <= i by FINSEQ_1: 1;



 A187: i <= n by A185, FINSEQ_1: 1;



 A188: j in ( Seg n) by A181, A184, ZFMISC_1: 87;

 then

 A189: 1 <= j by FINSEQ_1: 1;



 A190: j <= n by A188, FINSEQ_1: 1;

 per cases by A186, XXREAL_0: 1;

 suppose

 A191: 1 < i;

 now

 per cases ;

 suppose

 A192: i <> j;



 A193: (( 1. (K,n)) * (i,j)) = (( Base_FinSeq (K,n,i0)) . j0) by A186, A187, A189, A190, Th27

 .= ( 0. K) by A189, A190, A192, Th25;



 thus ((Q * P) * (i,j)) = ((Q * P) * (i0,j0))

 .= (( 1. (K,n)) * (i,j)) by A115, A187, A189, A190, A191, A192, A193;

 end;

 suppose

 A194: i = j;



 A195: (( 1. (K,n)) * (i,j)) = (( Base_FinSeq (K,n,i0)) . j0) by A186, A187, A189, A190, Th27

 .= ( 1. K) by A189, A190, A194, Th24;



 thus ((Q * P) * (i,j)) = ((Q * P) * (i0,j0))

 .= (( 1. (K,n)) * (i,j)) by A71, A190, A191, A194, A195;

 end;

 end;

 hence thesis;

 end;

 suppose

 A196: 1 = i;

 now

 per cases ;

 suppose

 A197: i < j;



 A198: (( 1. (K,n)) * (i,j)) = (( Base_FinSeq (K,n,i0)) . j0) by A186, A187, A189, A190, Th27

 .= ( 0. K) by A189, A190, A197, Th25;



 thus ((Q * P) * (i,j)) = ((Q * P) * (i0,j0))

 .= (( 1. (K,n)) * (i,j)) by A35, A190, A196, A197, A198;

 end;

 suppose

 A199: i >= j;

 then

 A200: i = j by A189, A196, XXREAL_0: 1;

 (( 1. (K,n)) * (i,j)) = (( Base_FinSeq (K,n,i0)) . j0) by A186, A187, A189, A190, Th27

 .= ( 1. K) by A189, A190, A200, Th24;

 hence thesis by A183, A189, A196, A199, XXREAL_0: 1;

 end;

 end;

 hence thesis;

 end;

 end;

 then

 A201: (Q * P) = ( 1. (K,n)) by MATRIX_0: 27;



 A202: ( len Q) = n by MATRIX_0: 24;



 A203: ( len ( Base_FinSeq (K,n,1))) = n by Th23;



 A204: ( len (a * ( Base_FinSeq (K,n,1)))) = ( len ( Base_FinSeq (K,n,1))) by MATRIXR1: 16

 .= n by Th23;



 A205: for k be Nat st 1 <= k & k <= n holds (( Col (Q,1)) . k) = ((a * ( Base_FinSeq (K,n,1))) . k)

 proof

 let k be Nat;

 assume that

 A206: 1 <= k and

 A207: k <= n;



 A208: (( Base_FinSeq (K,n,1)) /. k) = (( Base_FinSeq (K,n,1)) . k) by A203, A206, A207, FINSEQ_4: 15;



 A209: k in ( dom (a * ( Base_FinSeq (K,n,1)))) by A204, A206, A207, FINSEQ_3: 25;

 A210:

 now

 assume

 A211: k <> 1;



 thus ((a * ( Base_FinSeq (K,n,1))) . k) = (a * (( Base_FinSeq (K,n,1)) /. k)) by A208, A209, FVSUM_1: 50

 .= (a * ( 0. K)) by A206, A207, A208, A211, Th25

 .= ( 0. K);

 end;



 A212: k in NAT by ORDINAL1:def 12;

 k in ( Seg n) by A206, A207, FINSEQ_1: 1;

 then

 A213: k in ( dom Q) by A202, FINSEQ_1:def 3;

 A214:

 now

 [k, 1] in ( Indices Q) by A8, A206, A207, MATRIX_0: 31;

 then

 A215: ex p be FinSequence of K st p = (Q . k) & (Q * (k,1)) = (p . 1) by MATRIX_0:def 5;

 assume

 A216: k <> 1;

 then 1 < k by A206, XXREAL_0: 1;



 then (Q * (k,1)) = (( Base_FinSeq (K,n,k)) . 1) by A7, A207, A212, A215

 .= ( 0. K) by A8, A216, Th25;

 hence (( Col (Q,1)) . k) = ( 0. K) by A213, MATRIX_0:def 8;

 end;

 A217:

 now

 assume

 A218: k = 1;



 thus ((a * ( Base_FinSeq (K,n,1))) . k) = (a * (( Base_FinSeq (K,n,1)) /. k)) by A208, A209, FVSUM_1: 50

 .= (a * ( 1. K)) by A207, A208, A218, Th24

 .= a;

 end;

 1 <= n by A206, A207, XXREAL_0: 2;

 then 1 in ( dom Q) by A202, FINSEQ_3: 25;

 hence thesis by A5, A210, A217, A214, MATRIX_0:def 8;

 end;



 A219: ( 0 + 1) <= n by A1, NAT_1: 13;



 A220: ( len P) = n by MATRIX_0: 24;

 then

 A221: 1 in ( Seg ( len P)) by A219, FINSEQ_1: 1;

 then

 A222: 1 in ( dom P) by FINSEQ_1:def 3;



 A223: ( width P) = n by MATRIX_0: 24;

 then

 A224: ( len ( Line (P,1))) = n by MATRIX_0:def 7;

 then

 A225: 1 in ( dom ( Line (P,1))) by A220, A221, FINSEQ_1:def 3;



 A226: 1 in ( Seg ( width P)) by A223, A219, FINSEQ_1: 1;



 A227: for j st 1 < j & j <= n holds ((P * Q) * (1,j)) = ( 0. K)

 proof

 let j;

 assume that

 A228: 1 < j and

 A229: j <= n;



 A230: ( len ( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1))))) = ( len (( - (a * (P * (1,j)))) * ( Base_FinSeq (K,n,1)))) by Th6

 .= ( len ( Base_FinSeq (K,n,1))) by MATRIXR1: 16

 .= n by Th23;

 reconsider p = ( Col (Q,j)), q = (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) + ( Base_FinSeq (K,n,j))) as FinSequence of K;



 A231: ( len ( Base_FinSeq (K,n,j))) = n by Th23;



 A232: ( len (( - (a * (P * (1,j)))) * ( Base_FinSeq (K,n,1)))) = ( len ( Base_FinSeq (K,n,1))) by MATRIXR1: 16

 .= n by Th23;



 A233: for k be Nat st 1 <= k & k <= n holds (p . k) = (q . k)

 proof

 let k be Nat;

 assume that

 A234: 1 <= k and

 A235: k <= n;



 A236: k in ( dom Q) by A202, A234, A235, FINSEQ_3: 25;

 ( len ( Base_FinSeq (K,n,1))) = n by Th23;

 then

 A237: (( Base_FinSeq (K,n,1)) /. k) = (( Base_FinSeq (K,n,1)) . k) by A234, A235, FINSEQ_4: 15;



 A238: k in ( dom (( - (a * (P * (1,j)))) * ( Base_FinSeq (K,n,1)))) & (( Base_FinSeq (K,n,1)) /. k) = (( Base_FinSeq (K,n,1)) . k) by A203, A232, A234, A235, FINSEQ_3: 25, FINSEQ_4: 15;



 A239: (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) = ((( - (a * (P * (1,j)))) * ( Base_FinSeq (K,n,1))) . k) by Th6

 .= (( - (a * (P * (1,j)))) * (( Base_FinSeq (K,n,1)) /. k)) by A238, FVSUM_1: 50;

 per cases by A234, XXREAL_0: 1;

 suppose

 A240: 1 = k;

 (( Base_FinSeq (K,n,j)) /. k) = (( Base_FinSeq (K,n,j)) . k) by A231, A234, A235, FINSEQ_4: 15

 .= ( 0. K) by A228, A235, A240, Th25;

 then (q . k) = ((( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) /. k) + ( 0. K)) by A230, A231, A234, A235, Th5;

 then

 A241: (q . k) = (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) /. k) by RLVECT_1: 4;



 A242: (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) = (( - (a * (P * (1,j)))) * ( 1_ K)) by A235, A239, A237, A240, Th24

 .= ( - (a * (P * (1,j))));

 (p . k) = (Q * (1,j)) by A236, A240, MATRIX_0:def 8

 .= ( - (a * (P * (1,j)))) by A6, A228, A229;

 hence thesis by A230, A234, A235, A242, A241, FINSEQ_4: 15;

 end;

 suppose

 A243: 1 < k;

 [k, j] in ( Indices Q) by A228, A229, A234, A235, MATRIX_0: 31;

 then

 consider p2 be FinSequence of K such that

 A244: p2 = (Q . k) and

 A245: (Q * (k,j)) = (p2 . j) by MATRIX_0:def 5;



 A246: k in NAT by ORDINAL1:def 12;



 A247: (p . k) = (p2 . j) by A236, A245, MATRIX_0:def 8

 .= (( Base_FinSeq (K,n,k)) . j) by A7, A235, A243, A244, A246;

 now

 per cases ;

 suppose

 A248: k <> j;

 (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) /. k) = (( - (a * (P * (1,j)))) * (( Base_FinSeq (K,n,1)) /. k)) by A230, A234, A235, A239, FINSEQ_4: 15

 .= (( - (a * (P * (1,j)))) * ( 0. K)) by A235, A237, A243, Th25

 .= ( 0. K);



 then (q . k) = (( 0. K) + (( Base_FinSeq (K,n,j)) /. k)) by A230, A231, A234, A235, Th5

 .= (( Base_FinSeq (K,n,j)) /. k) by RLVECT_1: 4

 .= (( Base_FinSeq (K,n,j)) . k) by A231, A234, A235, FINSEQ_4: 15

 .= ( 0. K) by A234, A235, A248, Th25;

 hence thesis by A228, A229, A247, A248, Th25;

 end;

 suppose

 A249: k = j;

 (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) /. k) = (( - (a * (P * (1,j)))) * (( Base_FinSeq (K,n,1)) /. k)) by A230, A234, A235, A239, FINSEQ_4: 15

 .= (( - (a * (P * (1,j)))) * ( 0. K)) by A235, A237, A243, Th25

 .= ( 0. K);



 then (q . k) = (( 0. K) + (( Base_FinSeq (K,n,j)) /. k)) by A230, A231, A234, A235, Th5

 .= (( Base_FinSeq (K,n,j)) /. k) by RLVECT_1: 4

 .= (( Base_FinSeq (K,n,j)) . k) by A231, A234, A235, FINSEQ_4: 15

 .= ( 1. K) by A234, A235, A249, Th24;

 hence thesis by A234, A235, A247, A249, Th24;

 end;

 end;

 hence thesis;

 end;

 end;



 A250: ( width P) = n by MATRIX_0: 24;

 then

 A251: ( len ( Line (P,1))) = n by MATRIX_0:def 7;



 then

 A252: (( Line (P,1)) /. 1) = (( Line (P,1)) . 1) by A219, FINSEQ_4: 15

 .= (a " ) by A3, A226, MATRIX_0:def 7;



 A253: j in ( Seg n) by A228, A229, FINSEQ_1: 1;



 A254: ( len ( Col (Q,j))) = ( len Q) by MATRIX_0:def 8

 .= n by MATRIX_0: 24;

 ( len (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) + ( Base_FinSeq (K,n,j)))) = n by A230, A231, Th2;

 then

 A255: ( Col (Q,j)) = (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) + ( Base_FinSeq (K,n,j))) by A254, A233, FINSEQ_1: 14;



 A256: (( Line (P,1)) /. j) = (( Line (P,1)) . j) by A228, A229, A251, FINSEQ_4: 15

 .= (P * (1,j)) by A253, A250, MATRIX_0:def 7;

 [1, j] in ( Indices (P * Q)) by A219, A228, A229, MATRIX_0: 31;



 then ((P * Q) * (1,j)) = |(( Line (P,1)), ( Col (Q,j)))| by A202, A250, MATRIX_3:def 4

 .= ( |(( Line (P,1)), ( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))))| + |(( Line (P,1)), ( Base_FinSeq (K,n,j)))|) by A224, A230, A231, A255, Th11

 .= ( |(( Line (P,1)), (( - (a * (P * (1,j)))) * ( Base_FinSeq (K,n,1))))| + |(( Line (P,1)), ( Base_FinSeq (K,n,j)))|) by Th6

 .= ((( - (a * (P * (1,j)))) * |(( Line (P,1)), ( Base_FinSeq (K,n,1)))|) + |(( Line (P,1)), ( Base_FinSeq (K,n,j)))|) by A224, A203, Th10

 .= ((( - (a * (P * (1,j)))) * (a " )) + |(( Line (P,1)), ( Base_FinSeq (K,n,j)))|) by A224, A219, A252, Th35

 .= (( - ((a * (P * (1,j))) * (a " ))) + |(( Line (P,1)), ( Base_FinSeq (K,n,j)))|) by VECTSP_1: 9

 .= (( - ((P * (1,j)) * (a * (a " )))) + |(( Line (P,1)), ( Base_FinSeq (K,n,j)))|) by GROUP_1:def 3

 .= (( - ((P * (1,j)) * ( 1_ K))) + |(( Line (P,1)), ( Base_FinSeq (K,n,j)))|) by A2, VECTSP_1:def 10

 .= (( - ((P * (1,j)) * ( 1. K))) + (( Line (P,1)) /. j)) by A224, A228, A229, Th35

 .= (( - (P * (1,j))) + (P * (1,j))) by A256

 .= ( 0. K) by RLVECT_1: 5;

 hence thesis;

 end;



 A257: ( Indices Q) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;



 A258: for i, j st 1 < i & i <= n & i = j holds ((P * Q) * (i,j)) = ( 1. K)

 proof

 let i, j;

 assume that

 A259: 1 < i and

 A260: i <= n and

 A261: i = j;



 A262: ( len ( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1))))) = ( len (( - (a * (P * (1,j)))) * ( Base_FinSeq (K,n,1)))) by Th6

 .= ( len ( Base_FinSeq (K,n,1))) by MATRIXR1: 16

 .= n by Th23;

 reconsider p = ( Col (Q,j)), q = (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) + ( Base_FinSeq (K,n,j))) as FinSequence of K;



 A263: ( len ( Base_FinSeq (K,n,j))) = n by Th23;



 A264: j in ( Seg n) by A259, A260, A261, FINSEQ_1: 1;



 A265: for k be Nat st 1 <= k & k <= n holds (p . k) = (q . k)

 proof



 A266: ( len (( - (a * (P * (1,j)))) * ( Base_FinSeq (K,n,1)))) = ( len ( Base_FinSeq (K,n,1))) by MATRIXR1: 16

 .= n by Th23;

 let k be Nat;

 assume that

 A267: 1 <= k and

 A268: k <= n;



 A269: k in ( Seg n) by A267, A268, FINSEQ_1: 1;

 ( len (( - (a * (P * (1,j)))) * ( Base_FinSeq (K,n,1)))) = ( len ( Base_FinSeq (K,n,1))) by MATRIXR1: 16

 .= n by Th23;

 then

 A270: k in ( dom (( - (a * (P * (1,j)))) * ( Base_FinSeq (K,n,1)))) by A267, A268, FINSEQ_3: 25;



 A271: (( Base_FinSeq (K,n,1)) /. k) = (( Base_FinSeq (K,n,1)) . k) by A203, A267, A268, FINSEQ_4: 15;

 ( len ( Base_FinSeq (K,n,1))) = n by Th23;

 then

 A272: (( Base_FinSeq (K,n,1)) /. k) = (( Base_FinSeq (K,n,1)) . k) by A267, A268, FINSEQ_4: 15;

 k in ( dom Q) by A202, A267, A268, FINSEQ_3: 25;

 then

 A273: (p . k) = (Q * (k,j)) by MATRIX_0:def 8;



 A274: (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) = ((( - (a * (P * (1,j)))) * ( Base_FinSeq (K,n,1))) . k) by Th6

 .= (( - (a * (P * (1,j)))) * (( Base_FinSeq (K,n,1)) /. k)) by A270, A271, FVSUM_1: 50;

 per cases by A267, XXREAL_0: 1;

 suppose

 A275: 1 = k;

 k <= ( len ( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1))))) by A268, A266, Th6;



 then

 A276: (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) /. k) = (( - (a * (P * (1,j)))) * (( Base_FinSeq (K,n,1)) /. k)) by A267, A274, FINSEQ_4: 15

 .= (( - (a * (P * (1,j)))) * ( 1. K)) by A219, A272, A275, Th24;

 (( Base_FinSeq (K,n,j)) /. k) = (( Base_FinSeq (K,n,j)) . k) by A263, A267, A268, FINSEQ_4: 15

 .= ( 0. K) by A259, A261, A268, A275, Th25;



 then (q . k) = ((( - (a * (P * (1,j)))) * ( 1. K)) + ( 0. K)) by A262, A263, A267, A268, A276, Th5

 .= (( - (a * (P * (1,j)))) * ( 1. K)) by RLVECT_1: 4

 .= ( - (a * (P * (1,j))));

 hence thesis by A6, A259, A260, A261, A273, A275;

 end;

 suppose

 A277: 1 < k;

 [k, j] in ( Indices Q) by A257, A264, A269, ZFMISC_1: 87;

 then

 A278: ex p2 be FinSequence of K st p2 = (Q . k) & (Q * (k,j)) = (p2 . j) by MATRIX_0:def 5;

 k in NAT by ORDINAL1:def 12;

 then

 A279: (p . k) = (( Base_FinSeq (K,n,k)) . j) by A7, A268, A273, A277, A278;

 now

 per cases ;

 suppose

 A280: k <> j;

 then

 A281: (p . k) = ( 0. K) by A259, A260, A261, A279, Th25;



 A282: (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) /. k) = (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) by A262, A267, A268, FINSEQ_4: 15;



 A283: (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) = (( - (a * (P * (1,j)))) * ( 0. K)) by A268, A271, A274, A277, Th25

 .= ( 0. K);

 (( Base_FinSeq (K,n,j)) /. k) = (( Base_FinSeq (K,n,j)) . k) by A263, A267, A268, FINSEQ_4: 15

 .= ( 0. K) by A267, A268, A280, Th25;

 then (q . k) = (( 0. K) + ( 0. K)) by A262, A263, A267, A268, A282, A283, Th5;

 hence thesis by A281, RLVECT_1: 4;

 end;

 suppose

 A284: k = j;

 then

 A285: (p . k) = ( 1. K) by A267, A268, A279, Th24;



 A286: (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) /. k) = (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) by A262, A267, A268, FINSEQ_4: 15;



 A287: (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) = (( - (a * (P * (1,j)))) * ( 0. K)) by A268, A271, A274, A277, Th25

 .= ( 0. K);

 (( Base_FinSeq (K,n,j)) /. k) = (( Base_FinSeq (K,n,j)) . k) by A263, A267, A268, FINSEQ_4: 15

 .= ( 1. K) by A259, A260, A261, A284, Th24;

 then (q . k) = (( 0. K) + ( 1. K)) by A262, A263, A267, A268, A286, A287, Th5;

 hence thesis by A285, RLVECT_1: 4;

 end;

 end;

 hence thesis;

 end;

 end;

 [i, j] in ( Indices P) by A259, A260, A261, MATRIX_0: 31;

 then

 consider p1 be FinSequence of K such that

 A288: p1 = (P . i) and

 A289: (P * (i,j)) = (p1 . j) by MATRIX_0:def 5;

 p1 = ( Base_FinSeq (K,n,i)) by A4, A259, A260, A288;

 then

 A290: (p1 . j) = ( 1. K) by A259, A260, A261, Th24;



 A291: ( len ( Col (Q,j))) = ( len Q) by MATRIX_0:def 8

 .= n by MATRIX_0: 24;

 ( len (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) + ( Base_FinSeq (K,n,j)))) = n by A262, A263, Th2;

 then

 A292: ( Col (Q,j)) = (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) + ( Base_FinSeq (K,n,j))) by A291, A265, FINSEQ_1: 14;



 A293: ( width P) = n by MATRIX_0: 24;

 then

 A294: ( len ( Line (P,i))) = n by MATRIX_0:def 7;



 then

 A295: (( Line (P,i)) /. 1) = (( Line (P,i)) . 1) by A219, FINSEQ_4: 15

 .= (P * (i,1)) by A226, MATRIX_0:def 7;



 A296: (( Line (P,i)) /. j) = (( Line (P,i)) . j) by A259, A260, A261, A294, FINSEQ_4: 15

 .= (P * (i,j)) by A264, A293, MATRIX_0:def 7;

 [i, j] in ( Indices (P * Q)) by A259, A260, A261, MATRIX_0: 31;



 then

 A297: ((P * Q) * (i,j)) = |(( Line (P,i)), ( Col (Q,j)))| by A202, A293, MATRIX_3:def 4

 .= ( |(( Line (P,i)), ( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))))| + |(( Line (P,i)), ( Base_FinSeq (K,n,j)))|) by A262, A263, A292, A294, Th11

 .= ( |(( Line (P,i)), (( - (a * (P * (1,j)))) * ( Base_FinSeq (K,n,1))))| + |(( Line (P,i)), ( Base_FinSeq (K,n,j)))|) by Th6

 .= ((( - (a * (P * (1,j)))) * |(( Line (P,i)), ( Base_FinSeq (K,n,1)))|) + |(( Line (P,i)), ( Base_FinSeq (K,n,j)))|) by A203, A294, Th10

 .= ((( - (a * (P * (1,j)))) * (P * (i,1))) + |(( Line (P,i)), ( Base_FinSeq (K,n,j)))|) by A219, A294, A295, Th35

 .= (( - ((a * (P * (1,j))) * (P * (i,1)))) + |(( Line (P,i)), ( Base_FinSeq (K,n,j)))|) by VECTSP_1: 9

 .= (( - ((P * (1,j)) * (a * (P * (i,1))))) + |(( Line (P,i)), ( Base_FinSeq (K,n,j)))|) by GROUP_1:def 3

 .= (( - ((P * (1,j)) * (a * (P * (i,1))))) + (P * (i,j))) by A259, A260, A261, A294, A296, Th35;



 A298: 1 <= n by A259, A260, XXREAL_0: 2;

 [i, 1] in ( Indices P) by A8, A259, A260, MATRIX_0: 31;

 then

 consider p2 be FinSequence of K such that

 A299: p2 = (P . i) and

 A300: (P * (i,1)) = (p2 . 1) by MATRIX_0:def 5;

 p2 = ( Base_FinSeq (K,n,i)) by A4, A259, A260, A299;



 hence ((P * Q) * (i,j)) = (( - ((P * (1,j)) * (a * ( 0. K)))) + (P * (i,j))) by A259, A298, A297, A300, Th25

 .= (( - ((P * (1,j)) * ( 0. K))) + (P * (i,j)))

 .= (( - ( 0. K)) + (P * (i,j)))

 .= (( 0. K) + ( 1. K)) by A289, A290, RLVECT_1: 12

 .= ( 1. K) by RLVECT_1: 4;

 end;

 ( len ( Col (Q,1))) = ( len Q) by MATRIX_0:def 8

 .= n by MATRIX_0: 24;

 then

 A301: ( Col (Q,1)) = (a * ( Base_FinSeq (K,n,1))) by A204, A205, FINSEQ_1: 14;



 A302: ( Indices (P * Q)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;



 A303: for i, j st 1 j holds ((P * Q) * (i,j)) = ( 0. K)

 proof



 A304: ( len (a * ( Base_FinSeq (K,n,1)))) = ( len ( Base_FinSeq (K,n,1))) by MATRIXR1: 16

 .= n by Th23;

 let i, j;

 assume that

 A305: 1 j;



 A310: [i, j] in ( Indices (P * Q)) by A305, A306, A307, A308, MATRIX_0: 31;



 A311: j in ( Seg n) by A307, A308, FINSEQ_1: 1;



 A312: ( len ( Col (Q,j))) = ( len Q) by MATRIX_0:def 8

 .= n by MATRIX_0: 24;



 A313: [i, 1] in ( Indices P) by A8, A305, A306, MATRIX_0: 31;



 A314: ( len ( Base_FinSeq (K,n,j))) = n by Th23;



 A315: ( len ( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1))))) = ( len (( - (a * (P * (1,j)))) * ( Base_FinSeq (K,n,1)))) by Th6

 .= ( len ( Base_FinSeq (K,n,1))) by MATRIXR1: 16

 .= n by Th23;

 then

 A316: ( len (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) + ( Base_FinSeq (K,n,j)))) = n by A314, Th2;



 A317: [i, j] in ( Indices P) by A305, A306, A307, A308, MATRIX_0: 31;

 now

 per cases ;

 suppose

 A318: j > 1;

 reconsider p = ( Col (Q,j)), q = (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) + ( Base_FinSeq (K,n,j))) as FinSequence of K;

 for k be Nat st 1 <= k & k <= n holds (p . k) = (q . k)

 proof

 let k be Nat;

 assume that

 A319: 1 <= k and

 A320: k <= n;



 A321: (( Base_FinSeq (K,n,1)) /. k) = (( Base_FinSeq (K,n,1)) . k) by A203, A319, A320, FINSEQ_4: 15;



 A322: ( len (( - (a * (P * (1,j)))) * ( Base_FinSeq (K,n,1)))) = ( len ( Base_FinSeq (K,n,1))) by MATRIXR1: 16

 .= n by Th23;

 then

 A323: k in ( dom (( - (a * (P * (1,j)))) * ( Base_FinSeq (K,n,1)))) by A319, A320, FINSEQ_3: 25;



 A324: (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) = ((( - (a * (P * (1,j)))) * ( Base_FinSeq (K,n,1))) . k) by Th6

 .= (( - (a * (P * (1,j)))) * (( Base_FinSeq (K,n,1)) /. k)) by A323, A321, FVSUM_1: 50;

 ( len ( Base_FinSeq (K,n,1))) = n by Th23;

 then

 A325: (( Base_FinSeq (K,n,1)) /. k) = (( Base_FinSeq (K,n,1)) . k) by A319, A320, FINSEQ_4: 15;

 k in ( dom Q) by A202, A319, A320, FINSEQ_3: 25;

 then

 A326: (p . k) = (Q * (k,j)) by MATRIX_0:def 8;

 per cases by A319, XXREAL_0: 1;

 suppose

 A327: 1 = k;

 k <= ( len ( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1))))) by A320, A322, Th6;



 then

 A328: (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) /. k) = (( - (a * (P * (1,j)))) * (( Base_FinSeq (K,n,1)) /. k)) by A319, A324, FINSEQ_4: 15

 .= (( - (a * (P * (1,j)))) * ( 1. K)) by A219, A325, A327, Th24;

 (( Base_FinSeq (K,n,j)) /. k) = (( Base_FinSeq (K,n,j)) . k) by A314, A319, A320, FINSEQ_4: 15

 .= ( 0. K) by A318, A320, A327, Th25;



 then (q . k) = ((( - (a * (P * (1,j)))) * ( 1. K)) + ( 0. K)) by A315, A314, A319, A320, A328, Th5

 .= (( - (a * (P * (1,j)))) * ( 1_ K)) by RLVECT_1: 4

 .= ( - (a * (P * (1,j))));

 hence thesis by A6, A308, A318, A326, A327;

 end;

 suppose

 A329: 1 < k;

 [k, j] in ( Indices Q) by A307, A308, A319, A320, MATRIX_0: 31;

 then

 A330: ex p2 be FinSequence of K st p2 = (Q . k) & (Q * (k,j)) = (p2 . j) by MATRIX_0:def 5;

 k in NAT by ORDINAL1:def 12;

 then

 A331: (p . k) = (( Base_FinSeq (K,n,k)) . j) by A7, A320, A326, A329, A330;



 A332: k <= ( len ( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1))))) by A320, A322, Th6;

 now

 per cases ;

 suppose

 A333: k <> j;

 (( Base_FinSeq (K,n,j)) /. k) = (( Base_FinSeq (K,n,j)) . k) by A314, A319, A320, FINSEQ_4: 15

 .= ( 0. K) by A319, A320, A333, Th25;

 then (q . k) = ((( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) /. k) + ( 0. K)) by A315, A314, A319, A320, Th5;



 then

 A334: (q . k) = (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) /. k) by RLVECT_1: 4

 .= (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) by A319, A332, FINSEQ_4: 15;

 (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) = (( - (a * (P * (1,j)))) * ( 0. K)) by A320, A324, A325, A329, Th25

 .= ( 0. K);

 hence thesis by A307, A308, A331, A333, A334, Th25;

 end;

 suppose

 A335: k = j;

 then

 A336: (p . k) = ( 1. K) by A319, A320, A331, Th24;



 A337: (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) /. k) = (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) by A315, A319, A320, FINSEQ_4: 15;



 A338: (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) = (( - (a * (P * (1,j)))) * ( 0. K)) by A320, A321, A324, A329, Th25

 .= ( 0. K);

 (( Base_FinSeq (K,n,j)) /. k) = (( Base_FinSeq (K,n,j)) . k) by A314, A319, A320, FINSEQ_4: 15

 .= ( 1. K) by A319, A320, A335, Th24;

 then (q . k) = (( 0. K) + ( 1. K)) by A315, A314, A319, A320, A337, A338, Th5;

 hence thesis by A336, RLVECT_1: 4;

 end;

 end;

 hence thesis;

 end;

 end;

 then

 A339: ( Col (Q,j)) = (( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))) + ( Base_FinSeq (K,n,j))) by A312, A316, FINSEQ_1: 14;



 A340: 1 <= n by A305, A306, XXREAL_0: 2;



 A341: ( width P) = n by MATRIX_0: 24;

 then

 A342: ( len ( Line (P,i))) = n by MATRIX_0:def 7;



 then

 A343: (( Line (P,i)) /. j) = (( Line (P,i)) . j) by A307, A308, FINSEQ_4: 15

 .= (P * (i,j)) by A311, A341, MATRIX_0:def 7;



 A344: (( Line (P,i)) /. 1) = (( Line (P,i)) . 1) by A219, A342, FINSEQ_4: 15

 .= (P * (i,1)) by A226, MATRIX_0:def 7;



 A345: ((P * Q) * (i,j)) = |(( Line (P,i)), ( Col (Q,j)))| by A202, A310, A341, MATRIX_3:def 4

 .= ( |(( Line (P,i)), ( - ((a * (P * (1,j))) * ( Base_FinSeq (K,n,1)))))| + |(( Line (P,i)), ( Base_FinSeq (K,n,j)))|) by A315, A314, A339, A342, Th11

 .= ( |(( Line (P,i)), (( - (a * (P * (1,j)))) * ( Base_FinSeq (K,n,1))))| + |(( Line (P,i)), ( Base_FinSeq (K,n,j)))|) by Th6

 .= ((( - (a * (P * (1,j)))) * |(( Line (P,i)), ( Base_FinSeq (K,n,1)))|) + |(( Line (P,i)), ( Base_FinSeq (K,n,j)))|) by A203, A342, Th10

 .= ((( - (a * (P * (1,j)))) * (P * (i,1))) + |(( Line (P,i)), ( Base_FinSeq (K,n,j)))|) by A219, A342, A344, Th35

 .= (( - ((a * (P * (1,j))) * (P * (i,1)))) + |(( Line (P,i)), ( Base_FinSeq (K,n,j)))|) by VECTSP_1: 9

 .= (( - ((P * (1,j)) * (a * (P * (i,1))))) + |(( Line (P,i)), ( Base_FinSeq (K,n,j)))|) by GROUP_1:def 3

 .= (( - ((P * (1,j)) * (a * (P * (i,1))))) + (P * (i,j))) by A307, A308, A342, A343, Th35;

 consider p2 be FinSequence of K such that

 A346: p2 = (P . i) and

 A347: (P * (i,1)) = (p2 . 1) by A313, MATRIX_0:def 5;

 consider p1 be FinSequence of K such that

 A348: p1 = (P . i) and

 A349: (P * (i,j)) = (p1 . j) by A317, MATRIX_0:def 5;

 p1 = ( Base_FinSeq (K,n,i)) by A4, A305, A306, A348;

 then

 A350: (p1 . j) = ( 0. K) by A307, A308, A309, Th25;

 p2 = ( Base_FinSeq (K,n,i)) by A4, A305, A306, A346;



 then ((P * Q) * (i,j)) = (( - ((P * (1,j)) * (a * ( 0. K)))) + (P * (i,j))) by A305, A340, A345, A347, Th25

 .= (( - ((P * (1,j)) * ( 0. K))) + (P * (i,j)))

 .= (( - ( 0. K)) + (P * (i,j)))

 .= (( 0. K) + ( 0. K)) by A349, A350, RLVECT_1: 12

 .= ( 0. K) by RLVECT_1: 4;

 hence thesis;

 end;

 suppose

 A351: j <= 1;

 reconsider p = ( Col (Q,j)), q = (a * ( Base_FinSeq (K,n,1))) as FinSequence of K;



 A352: for k be Nat st 1 <= k & k <= n holds (p . k) = (q . k)

 proof

 let k be Nat;

 assume that

 A353: 1 <= k and

 A354: k <= n;



 A355: k in ( dom Q) by A202, A353, A354, FINSEQ_3: 25;



 A356: ( len ( Base_FinSeq (K,n,1))) = n by Th23;

 then

 A357: (( Base_FinSeq (K,n,1)) /. k) = (( Base_FinSeq (K,n,1)) . k) by A353, A354, FINSEQ_4: 15;

 k in ( dom (a * ( Base_FinSeq (K,n,1)))) by A204, A353, A354, FINSEQ_3: 25;

 then

 A358: ((a * ( Base_FinSeq (K,n,1))) . k) = (a * (( Base_FinSeq (K,n,1)) /. k)) by A357, FVSUM_1: 50;

 per cases by A353, XXREAL_0: 1;

 suppose

 A359: 1 = k;



 then

 A360: (q . k) = (a * ( 1. K)) by A354, A357, A358, Th24

 .= a;

 (p . k) = (Q * (1,j)) by A355, A359, MATRIX_0:def 8

 .= a by A5, A307, A351, XXREAL_0: 1;

 hence thesis by A360;

 end;

 suppose

 A361: 1 < k;

 [k, j] in ( Indices Q) by A307, A308, A353, A354, MATRIX_0: 31;

 then

 A362: ex p2 be FinSequence of K st p2 = (Q . k) & (Q * (k,j)) = (p2 . j) by MATRIX_0:def 5;



 A363: k in NAT by ORDINAL1:def 12;



 A364: (p . k) = (Q * (k,j)) by A355, MATRIX_0:def 8

 .= (( Base_FinSeq (K,n,k)) . j) by A7, A354, A361, A362, A363;

 now

 per cases ;

 suppose

 A365: k <> j;

 (( Base_FinSeq (K,n,1)) /. k) = (( Base_FinSeq (K,n,1)) . k) by A353, A354, A356, FINSEQ_4: 15;



 then (a * (( Base_FinSeq (K,n,1)) /. k)) = (a * ( 0. K)) by A354, A361, Th25

 .= ( 0. K);

 hence thesis by A307, A308, A358, A364, A365, Th25;

 end;

 suppose k = j;

 hence thesis by A351, A361;

 end;

 end;

 hence thesis;

 end;

 end;



 A366: 1 <= n by A305, A306, XXREAL_0: 2;



 A367: ( len ( Line (P,i))) = n by A223, MATRIX_0:def 7;



 then

 A368: (( Line (P,i)) /. 1) = (( Line (P,i)) . 1) by A219, FINSEQ_4: 15

 .= (P * (i,1)) by A226, MATRIX_0:def 7;



 A369: ((P * Q) * (i,j)) = |(( Line (P,i)), ( Col (Q,j)))| by A202, A223, A310, MATRIX_3:def 4

 .= |(( Line (P,i)), (a * ( Base_FinSeq (K,n,1))))| by A312, A304, A352, FINSEQ_1: 14

 .= (a * |(( Line (P,i)), ( Base_FinSeq (K,n,1)))|) by A203, A367, Th10

 .= (a * (P * (i,1))) by A219, A367, A368, Th35;

 consider p2 be FinSequence of K such that

 A370: p2 = (P . i) and

 A371: (P * (i,1)) = (p2 . 1) by A313, MATRIX_0:def 5;

 p2 = ( Base_FinSeq (K,n,i)) by A4, A305, A306, A370;



 hence ((P * Q) * (i,j)) = (a * ( 0. K)) by A305, A366, A369, A371, Th25

 .= ( 0. K);

 end;

 end;

 hence thesis;

 end;



 A372: ( len (a * ( Line (P,1)))) = ( len ( Line (P,1))) by MATRIXR1: 16

 .= n by A223, MATRIX_0:def 7;

 ( Indices P) = [:( Seg n), ( Seg n):] & [1, 1] in ( Indices P) by A219, MATRIX_0: 24, MATRIX_0: 31;



 then

 A373: ((P * Q) * (1,1)) = |(( Line (P,1)), ( Col (Q,1)))| by A202, A223, A302, MATRIX_3:def 4

 .= (a * |(( Line (P,1)), ( Base_FinSeq (K,n,1)))|) by A224, A203, A301, Th10

 .= (a * (( Line (P,1)) /. 1)) by A224, A219, Th35

 .= ((a * ( Line (P,1))) /. 1) by A225, POLYNOM1:def 1

 .= ((a * ( Line (P,1))) . 1) by A219, A372, FINSEQ_4: 15

 .= (a * (P * (1,1))) by A226, A222, MATRIX12: 3

 .= ( 1. K) by A2, A3, VECTSP_1:def 10;

 for i,j be Nat st [i, j] in ( Indices (P * Q)) holds ((P * Q) * (i,j)) = (( 1. (K,n)) * (i,j))

 proof

 let i,j be Nat;

 reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def 12;

 assume

 A374: [i, j] in ( Indices (P * Q));

 then

 A375: i in ( Seg n) by A302, ZFMISC_1: 87;

 then

 A376: 1 <= i by FINSEQ_1: 1;



 A377: i <= n by A375, FINSEQ_1: 1;



 A378: j in ( Seg n) by A302, A374, ZFMISC_1: 87;

 then

 A379: 1 <= j by FINSEQ_1: 1;



 A380: j <= n by A378, FINSEQ_1: 1;

 per cases by A376, XXREAL_0: 1;

 suppose

 A381: 1 < i;

 now

 per cases ;

 suppose

 A382: i <> j;



 A383: (( 1. (K,n)) * (i,j)) = (( Base_FinSeq (K,n,i0)) . j0) by A376, A377, A379, A380, Th27

 .= ( 0. K) by A379, A380, A382, Th25;



 thus ((P * Q) * (i,j)) = ((P * Q) * (i0,j0))

 .= (( 1. (K,n)) * (i,j)) by A303, A377, A379, A380, A381, A382, A383;

 end;

 suppose

 A384: i = j;



 A385: (( 1. (K,n)) * (i,j)) = (( Base_FinSeq (K,n,i0)) . j0) by A376, A377, A379, A380, Th27

 .= ( 1. K) by A379, A380, A384, Th24;



 thus ((P * Q) * (i,j)) = ((P * Q) * (i0,j0))

 .= (( 1. (K,n)) * (i,j)) by A258, A380, A381, A384, A385;

 end;

 end;

 hence thesis;

 end;

 suppose

 A386: 1 = i;

 now

 per cases ;

 suppose

 A387: i < j;



 A388: (( 1. (K,n)) * (i,j)) = (( Base_FinSeq (K,n,i0)) . j0) by A376, A377, A379, A380, Th27

 .= ( 0. K) by A379, A380, A387, Th25;



 thus ((P * Q) * (i,j)) = ((P * Q) * (i0,j0))

 .= (( 1. (K,n)) * (i,j)) by A227, A380, A386, A387, A388;

 end;

 suppose

 A389: i >= j;

 then

 A390: i = j by A379, A386, XXREAL_0: 1;

 (( 1. (K,n)) * (i,j)) = (( Base_FinSeq (K,n,i0)) . j0) by A376, A377, A379, A380, Th27

 .= ( 1. K) by A379, A380, A390, Th24;

 hence thesis by A373, A379, A386, A389, XXREAL_0: 1;

 end;

 end;

 hence thesis;

 end;

 end;

 then

 A391: (P * Q) = ( 1. (K,n)) by MATRIX_0: 27;

 hence P is invertible by A201, Th19;

 thus thesis by A391, A201, Th18;

 end;

 theorem :: MATRIX14:38



 Th38: for a be Element of K, P be Matrix of n, K st n > 0 & a <> ( 0. K) & (P * (1,1)) = (a " ) & (for i st 1 0 and

 A2: a <> ( 0. K) & (P * (1,1)) = (a " ) & for i st 1 1 implies $3 = ( - (a * (P * (1,$2))))))) & ($1 <> 1 implies for i0 be Element of NAT st i0 = $1 holds $3 = (( Base_FinSeq (K,n,i0)) . $2));



 A3: for i,j be Nat st [i, j] in [:( Seg n), ( Seg n):] holds ex x be Element of K st P[i, j, x]

 proof

 let i,j be Nat;

 reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def 12;

 assume [i, j] in [:( Seg n), ( Seg n):];

 then j0 in ( Seg n) by ZFMISC_1: 87;

 then

 A4: 1 <= j0 & j0 <= n by FINSEQ_1: 1;

 per cases ;

 suppose

 A5: i = 1;

 now

 per cases ;

 case

 A6: j = 1;

 set x1 = a;

 thus (i = 1 implies (j = 1 implies x1 = a) & (j <> 1 implies x1 = ( - (a * (P * (1,j)))))) & (i <> 1 implies for i1 be Element of NAT st i1 = i holds x1 = (( Base_FinSeq (K,n,i1)) . j)) by A5, A6;

 end;

 case

 A7: j <> 1;

 set x1 = ( - (a * (P * (1,j))));

 thus (i = 1 implies (j = 1 implies x1 = a) & (j <> 1 implies x1 = ( - (a * (P * (1,j)))))) & (i <> 1 implies for i1 be Element of NAT st i1 = i holds x1 = (( Base_FinSeq (K,n,i1)) . j)) by A5, A7;

 end;

 end;

 hence thesis;

 end;

 suppose

 A8: i <> 1;

 ( len ( Base_FinSeq (K,n,i0))) = n by Th23;

 then (( Base_FinSeq (K,n,i0)) /. j0) = (( Base_FinSeq (K,n,i0)) . j0) by A4, FINSEQ_4: 15;

 then

 reconsider x1 = (( Base_FinSeq (K,n,i0)) . j0) as Element of K;

 i <> 1 implies for i1 be Element of NAT st i1 = i holds x1 = (( Base_FinSeq (K,n,i1)) . j);

 hence thesis by A8;

 end;

 end;

 consider Q0 be Matrix of n, n, K such that

 A9: for i,j be Nat st [i, j] in ( Indices Q0) holds P[i, j, (Q0 * (i,j))] from MATRIX_0:sch 2( A3);



 A10: ( 0 + 1) <= n by A1, NAT_1: 13;



 A11: for j st 1 < j & j <= n holds (Q0 * (1,j)) = ( - (a * (P * (1,j))))

 proof

 let j;

 assume that

 A12: 1 < j and

 A13: j <= n;

 [1, j] in ( Indices Q0) by A10, A12, A13, MATRIX_0: 31;

 hence thesis by A9, A12;

 end;



 A14: ( Indices Q0) = [:( Seg n), ( Seg n):] & 1 in ( Seg n) by A10, FINSEQ_1: 1, MATRIX_0: 24;



 A15: for i st 1 < i & i <= n holds (Q0 . i) = ( Base_FinSeq (K,n,i))

 proof

 let i;

 assume that

 A16: 1 < i and

 A17: i <= n;

 i in ( Seg n) by A16, A17, FINSEQ_1: 1;

 then [i, 1] in ( Indices Q0) by A14, ZFMISC_1: 87;

 then

 consider p be FinSequence of K such that

 A18: p = (Q0 . i) and (Q0 * (i,1)) = (p . 1) by MATRIX_0:def 5;



 A19: for j be Nat st 1 <= j & j <= n holds (p . j) = (( Base_FinSeq (K,n,i)) . j)

 proof

 let j be Nat;

 assume 1 <= j & j <= n;

 then

 A20: [i, j] in ( Indices Q0) by A16, A17, MATRIX_0: 31;

 then ex p2 be FinSequence of K st p2 = (Q0 . i) & (Q0 * (i,j)) = (p2 . j) by MATRIX_0:def 5;

 hence thesis by A9, A16, A18, A20;

 end;

 ( len Q0) = n by MATRIX_0:def 2;

 then i in ( Seg ( len Q0)) by A16, A17, FINSEQ_1: 1;

 then i in ( dom Q0) by FINSEQ_1:def 3;

 then p in ( rng Q0) by A18, FUNCT_1:def 3;

 then

 A21: ( len p) = n by MATRIX_0:def 2;

 ( len ( Base_FinSeq (K,n,i))) = n by Th23;

 hence thesis by A18, A21, A19, FINSEQ_1: 14;

 end;

 [1, 1] in ( Indices Q0) by A10, MATRIX_0: 31;

 then (Q0 * (1,1)) = a by A9;

 hence thesis by A1, A2, A11, A15, Th37;

 end;

 theorem :: MATRIX14:39



 Th39: for A be Matrix of n, K st n > 0 & (A * (1,1)) <> ( 0. K) holds ex P be Matrix of n, K st P is invertible & ((A * P) * (1,1)) = ( 1. K) & (for j st 1 < j & j <= n holds ((A * P) * (1,j)) = ( 0. K)) & for i st 1 0 and

 A2: (A * (1,1)) <> ( 0. K);



 A3: ( 0 + 1) <= n by A1, NAT_1: 13;

 set a = (A * (1,1));

 defpred P[ Nat, Nat, Element of K] means ($1 = 1 implies (($2 = 1 implies $3 = (a " )) & ($2 <> 1 implies $3 = ( - ((a " ) * (A * (1,$2))))))) & ($1 <> 1 implies for i0 be Element of NAT st i0 = $1 holds $3 = (( Base_FinSeq (K,n,i0)) . $2));



 A4: for i,j be Nat st [i, j] in [:( Seg n), ( Seg n):] holds ex x be Element of K st P[i, j, x]

 proof

 let i,j be Nat;

 reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def 12;

 assume [i, j] in [:( Seg n), ( Seg n):];

 then j0 in ( Seg n) by ZFMISC_1: 87;

 then

 A5: 1 <= j0 & j0 <= n by FINSEQ_1: 1;

 per cases ;

 suppose

 A6: i = 1;

 per cases ;

 suppose j = 1;

 hence thesis by A6;

 end;

 suppose j <> 1;

 hence thesis by A6;

 end;

 end;

 suppose

 A7: i <> 1;

 set x1 = (( Base_FinSeq (K,n,i0)) /. j0);

 ( len ( Base_FinSeq (K,n,i0))) = n by Th23;

 then for i1 be Element of NAT st i1 = i holds x1 = (( Base_FinSeq (K,n,i1)) . j) by A5, FINSEQ_4: 15;

 hence thesis by A7;

 end;

 end;

 consider P0 be Matrix of n, n, K such that

 A8: for i,j be Nat st [i, j] in ( Indices P0) holds P[i, j, (P0 * (i,j))] from MATRIX_0:sch 2( A4);



 A9: ( 0 + 1) <= n by A1, NAT_1: 13;



 A10: for i st 1 < i & i <= n holds (P0 . i) = ( Base_FinSeq (K,n,i))

 proof

 let i;

 assume that

 A11: 1 < i and

 A12: i <= n;

 [i, 1] in ( Indices P0) by A9, A11, A12, MATRIX_0: 31;

 then

 consider p be FinSequence of K such that

 A13: p = (P0 . i) and (P0 * (i,1)) = (p . 1) by MATRIX_0:def 5;



 A14: for j be Nat st 1 <= j & j <= n holds (p . j) = (( Base_FinSeq (K,n,i)) . j)

 proof

 let j be Nat;

 assume 1 <= j & j <= n;

 then

 A15: [i, j] in ( Indices P0) by A11, A12, MATRIX_0: 31;

 then ex p2 be FinSequence of K st p2 = (P0 . i) & (P0 * (i,j)) = (p2 . j) by MATRIX_0:def 5;

 hence thesis by A8, A11, A13, A15;

 end;

 ( len P0) = n by MATRIX_0:def 2;

 then i in ( Seg ( len P0)) by A11, A12, FINSEQ_1: 1;

 then i in ( dom P0) by FINSEQ_1:def 3;

 then p in ( rng P0) by A13, FUNCT_1:def 3;

 then

 A16: ( len p) = n by MATRIX_0:def 2;

 ( len ( Base_FinSeq (K,n,i))) = n by Th23;

 hence thesis by A13, A16, A14, FINSEQ_1: 14;

 end;



 A17: ( len ((a " ) * ( Base_FinSeq (K,n,1)))) = ( len ( Base_FinSeq (K,n,1))) by MATRIXR1: 16

 .= n by Th23;



 A18: ( Indices P0) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;



 A19: ( len ( Base_FinSeq (K,n,1))) = n by Th23;



 A20: [1, 1] in ( Indices P0) by A9, MATRIX_0: 31;

 then

 A21: (P0 * (1,1)) = (a " ) by A8;

 then

 A22: P0 is invertible by A1, A2, A10, Th38;



 A23: ( len P0) = n by MATRIX_0: 24;

 then

 A24: 1 in ( Seg ( len P0)) by A9, FINSEQ_1: 1;



 A25: for k be Nat st 1 <= k & k <= n holds (( Col (P0,1)) . k) = (((a " ) * ( Base_FinSeq (K,n,1))) . k)

 proof

 let k be Nat;

 assume that

 A26: 1 <= k and

 A27: k <= n;



 A28: (( Base_FinSeq (K,n,1)) /. k) = (( Base_FinSeq (K,n,1)) . k) by A19, A26, A27, FINSEQ_4: 15;

 k in ( Seg n) by A26, A27, FINSEQ_1: 1;

 then

 A29: k in ( dom ((a " ) * ( Base_FinSeq (K,n,1)))) by A17, FINSEQ_1:def 3;

 A30:

 now

 assume

 A31: k <> 1;



 thus (((a " ) * ( Base_FinSeq (K,n,1))) . k) = ((a " ) * (( Base_FinSeq (K,n,1)) /. k)) by A29, A28, FVSUM_1: 50

 .= ((a " ) * ( 0. K)) by A26, A27, A28, A31, Th25

 .= ( 0. K);

 end;

 k in ( Seg n) by A26, A27, FINSEQ_1: 1;

 then

 A32: k in ( dom P0) by A23, FINSEQ_1:def 3;

 A33:

 now

 k in ( Seg n) by A26, A27, FINSEQ_1: 1;

 then [k, 1] in ( Indices P0) by A23, A24, A18, ZFMISC_1: 87;

 then

 A34: ex p be FinSequence of K st p = (P0 . k) & (P0 * (k,1)) = (p . 1) by MATRIX_0:def 5;

 assume

 A35: k <> 1;

 then k in NAT & 1 < k by A26, ORDINAL1:def 12, XXREAL_0: 1;



 then (P0 * (k,1)) = (( Base_FinSeq (K,n,k)) . 1) by A10, A27, A34

 .= ( 0. K) by A9, A35, Th25;

 hence (( Col (P0,1)) . k) = ( 0. K) by A32, MATRIX_0:def 8;

 end;

 A36:

 now

 assume

 A37: k = 1;



 hence (((a " ) * ( Base_FinSeq (K,n,1))) . k) = ((a " ) * (( Base_FinSeq (K,n,1)) /. 1)) by A29, A28, FVSUM_1: 50

 .= ((a " ) * ( 1. K)) by A27, A28, A37, Th24

 .= (a " );

 end;

 1 <= n by A26, A27, XXREAL_0: 2;

 then 1 in ( dom P0) by A23, FINSEQ_3: 25;

 hence thesis by A21, A30, A36, A33, MATRIX_0:def 8;

 end;



 A38: ( len A) = n by MATRIX_0: 24;

 then

 A39: 1 in ( Seg ( len A)) by A3, FINSEQ_1: 1;

 then

 A40: 1 in ( dom A) by FINSEQ_1:def 3;



 A41: ( width A) = n by MATRIX_0: 24;

 then

 A42: ( len ( Line (A,1))) = n by MATRIX_0:def 7;

 then

 A43: 1 in ( dom ( Line (A,1))) by A38, A39, FINSEQ_1:def 3;



 A44: 1 in ( Seg ( width A)) by A41, A3, FINSEQ_1: 1;



 A45: for i st 1 < i & i <= n & (A * (i,1)) = ( 0. K) holds ((A * P0) * (i,1)) = ( 0. K)

 proof

 set Q = A, P = P0;

 let i;

 assume that

 A46: 1 < i & i <= n and

 A47: (A * (i,1)) = ( 0. K);



 A48: 1 <= n by A46, XXREAL_0: 2;

 reconsider p = ( Col (P,1)), q = ((a " ) * ( Base_FinSeq (K,n,1))) as FinSequence of K;



 A49: ( len ( Col (P,1))) = ( len P) by MATRIX_0:def 8

 .= n by MATRIX_0: 24;



 A50: ( len ((a " ) * ( Base_FinSeq (K,n,1)))) = ( len ( Base_FinSeq (K,n,1))) by MATRIXR1: 16

 .= n by Th23;



 A51: for k be Nat st 1 <= k & k <= n holds (p . k) = (q . k)

 proof

 let k be Nat;

 assume that

 A52: 1 <= k and

 A53: k <= n;



 A54: ( len ( Base_FinSeq (K,n,1))) = n by Th23;

 then

 A55: (( Base_FinSeq (K,n,1)) /. k) = (( Base_FinSeq (K,n,1)) . k) by A52, A53, FINSEQ_4: 15;

 k in ( dom P) by A23, A52, A53, FINSEQ_3: 25;

 then

 A56: (p . k) = (P * (k,1)) by MATRIX_0:def 8;

 k in ( dom ((a " ) * ( Base_FinSeq (K,n,1)))) by A50, A52, A53, FINSEQ_3: 25;

 then

 A57: (((a " ) * ( Base_FinSeq (K,n,1))) . k) = ((a " ) * (( Base_FinSeq (K,n,1)) /. k)) by A55, FVSUM_1: 50;

 per cases by A52, XXREAL_0: 1;

 suppose

 A58: 1 = k;



 then (q . k) = ((a " ) * ( 1. K)) by A53, A55, A57, Th24

 .= (a " );

 hence thesis by A8, A20, A56, A58;

 end;

 suppose

 A59: 1 < k;

 (( Base_FinSeq (K,n,1)) /. k) = (( Base_FinSeq (K,n,1)) . k) by A52, A53, A54, FINSEQ_4: 15;



 then

 A60: ((a " ) * (( Base_FinSeq (K,n,1)) /. k)) = ((a " ) * ( 0. K)) by A53, A59, Th25

 .= ( 0. K);

 [k, 1] in ( Indices P) by A48, A52, A53, MATRIX_0: 31;

 then

 A61: ex p2 be FinSequence of K st p2 = (P . k) & (P * (k,1)) = (p2 . 1) by MATRIX_0:def 5;

 k in NAT by ORDINAL1:def 12;

 then (p . k) = (( Base_FinSeq (K,n,k)) . 1) by A10, A53, A56, A59, A61;

 hence thesis by A48, A57, A59, A60, Th25;

 end;

 end;



 A62: ( width Q) = n by MATRIX_0: 24;

 then

 A63: ( len ( Line (Q,i))) = n by MATRIX_0:def 7;



 then

 A64: (( Line (Q,i)) /. 1) = (( Line (Q,i)) . 1) by A3, FINSEQ_4: 15

 .= (Q * (i,1)) by A44, MATRIX_0:def 7;

 [i, 1] in ( Indices (Q * P)) by A46, A48, MATRIX_0: 31;



 hence ((Q * P) * (i,1)) = |(( Line (Q,i)), ( Col (P,1)))| by A23, A62, MATRIX_3:def 4

 .= |(( Line (Q,i)), ((a " ) * ( Base_FinSeq (K,n,1))))| by A49, A50, A51, FINSEQ_1: 14

 .= ((a " ) * |(( Line (Q,i)), ( Base_FinSeq (K,n,1)))|) by A19, A63, Th10

 .= ((a " ) * (Q * (i,1))) by A3, A63, A64, Th35

 .= ( 0. K) by A47;

 end;



 A65: for j st 1 < j & j <= n holds ((A * P0) * (1,j)) = ( 0. K)

 proof

 let j;

 assume that

 A66: 1 < j and

 A67: j <= n;



 A68: ( len ( Base_FinSeq (K,n,j))) = n by Th23;

 reconsider p = ( Col (P0,j)), q = (( - (((a " ) * (A * (1,j))) * ( Base_FinSeq (K,n,1)))) + ( Base_FinSeq (K,n,j))) as FinSequence of K;



 A69: ( len (( - ((a " ) * (A * (1,j)))) * ( Base_FinSeq (K,n,1)))) = ( len ( Base_FinSeq (K,n,1))) by MATRIXR1: 16

 .= n by Th23;



 A70: ( len ( - (((a " ) * (A * (1,j))) * ( Base_FinSeq (K,n,1))))) = ( len (( - ((a " ) * (A * (1,j)))) * ( Base_FinSeq (K,n,1)))) by Th6

 .= ( len ( Base_FinSeq (K,n,1))) by MATRIXR1: 16

 .= n by Th23;



 A71: [1, j] in ( Indices P0) by A9, A66, A67, MATRIX_0: 31;



 A72: for k be Nat st 1 <= k & k <= n holds (p . k) = (q . k)

 proof



 A73: ( len (( - ((a " ) * (A * (1,j)))) * ( Base_FinSeq (K,n,1)))) = ( len ( Base_FinSeq (K,n,1))) by MATRIXR1: 16

 .= n by Th23;

 let k be Nat;

 assume that

 A74: 1 <= k and

 A75: k <= n;

 k in ( Seg n) by A74, A75, FINSEQ_1: 1;

 then

 A76: k in ( dom (( - ((a " ) * (A * (1,j)))) * ( Base_FinSeq (K,n,1)))) by A69, FINSEQ_1:def 3;

 ( len ( Base_FinSeq (K,n,1))) = n by Th23;

 then

 A77: (( Base_FinSeq (K,n,1)) /. k) = (( Base_FinSeq (K,n,1)) . k) by A74, A75, FINSEQ_4: 15;



 A78: (( - (((a " ) * (A * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) = ((( - ((a " ) * (A * (1,j)))) * ( Base_FinSeq (K,n,1))) . k) by Th6

 .= (( - ((a " ) * (A * (1,j)))) * (( Base_FinSeq (K,n,1)) /. k)) by A76, A77, FVSUM_1: 50;

 ( len ( Base_FinSeq (K,n,1))) = n by Th23;

 then

 A79: (( Base_FinSeq (K,n,1)) /. k) = (( Base_FinSeq (K,n,1)) . k) by A74, A75, FINSEQ_4: 15;

 k in ( dom P0) by A23, A74, A75, FINSEQ_3: 25;

 then

 A80: (p . k) = (P0 * (k,j)) by MATRIX_0:def 8;

 per cases by A74, XXREAL_0: 1;

 suppose

 A81: 1 = k;

 k <= ( len ( - (((a " ) * (A * (1,j))) * ( Base_FinSeq (K,n,1))))) by A75, A73, Th6;



 then

 A82: (( - (((a " ) * (A * (1,j))) * ( Base_FinSeq (K,n,1)))) /. k) = (( - ((a " ) * (A * (1,j)))) * (( Base_FinSeq (K,n,1)) /. k)) by A74, A78, FINSEQ_4: 15

 .= (( - ((a " ) * (A * (1,j)))) * ( 1. K)) by A75, A79, A81, Th24

 .= ( - ((a " ) * (A * (1,j))));



 A83: (p . k) = ( - ((a " ) * (A * (1,j)))) by A8, A66, A71, A80, A81;

 (( Base_FinSeq (K,n,j)) /. k) = (( Base_FinSeq (K,n,j)) . k) by A68, A74, A75, FINSEQ_4: 15

 .= ( 0. K) by A66, A75, A81, Th25;

 then (q . k) = (( - ((a " ) * (A * (1,j)))) + ( 0. K)) by A70, A68, A74, A75, A82, Th5;

 hence thesis by A83, RLVECT_1: 4;

 end;

 suppose

 A84: 1 < k;

 [k, j] in ( Indices P0) & k in NAT by A66, A67, A74, A75, MATRIX_0: 31, ORDINAL1:def 12;

 then

 A85: (p . k) = (( Base_FinSeq (K,n,k)) . j) by A8, A80, A84;

 per cases ;

 suppose

 A86: k <> j;

 ( len ( Base_FinSeq (K,n,1))) = n by Th23;

 then (( Base_FinSeq (K,n,1)) /. k) = (( Base_FinSeq (K,n,1)) . k) by A74, A75, FINSEQ_4: 15;



 then

 A87: (( - (((a " ) * (A * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) = (( - ((a " ) * (A * (1,j)))) * ( 0. K)) by A75, A78, A84, Th25

 .= ( 0. K);



 A88: (( - (((a " ) * (A * (1,j))) * ( Base_FinSeq (K,n,1)))) /. k) = (( - (((a " ) * (A * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) by A70, A74, A75, FINSEQ_4: 15;



 A89: (p . k) = ( 0. K) by A66, A67, A85, A86, Th25;

 (( Base_FinSeq (K,n,j)) /. k) = (( Base_FinSeq (K,n,j)) . k) by A68, A74, A75, FINSEQ_4: 15

 .= ( 0. K) by A74, A75, A86, Th25;

 then (q . k) = (( 0. K) + ( 0. K)) by A70, A68, A74, A75, A88, A87, Th5;

 hence thesis by A89, RLVECT_1: 4;

 end;

 suppose

 A90: k = j;

 ( len ( Base_FinSeq (K,n,1))) = n by Th23;

 then (( Base_FinSeq (K,n,1)) /. k) = (( Base_FinSeq (K,n,1)) . k) by A74, A75, FINSEQ_4: 15;



 then

 A91: (( - (((a " ) * (A * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) = (( - ((a " ) * (A * (1,j)))) * ( 0. K)) by A75, A78, A84, Th25

 .= ( 0. K);



 A92: (( - (((a " ) * (A * (1,j))) * ( Base_FinSeq (K,n,1)))) /. k) = (( - (((a " ) * (A * (1,j))) * ( Base_FinSeq (K,n,1)))) . k) by A70, A74, A75, FINSEQ_4: 15;



 A93: (p . k) = ( 1. K) by A74, A75, A85, A90, Th24;

 (( Base_FinSeq (K,n,j)) /. k) = (( Base_FinSeq (K,n,j)) . k) by A68, A74, A75, FINSEQ_4: 15

 .= ( 1. K) by A74, A75, A90, Th24;

 then (q . k) = (( 0. K) + ( 1. K)) by A70, A68, A74, A75, A92, A91, Th5;

 hence thesis by A93, RLVECT_1: 4;

 end;

 end;

 end;



 A94: ( width A) = n by MATRIX_0: 24;

 then

 A95: ( len ( Line (A,1))) = n by MATRIX_0:def 7;



 then

 A96: (( Line (A,1)) /. 1) = (( Line (A,1)) . 1) by A3, FINSEQ_4: 15

 .= a by A44, MATRIX_0:def 7;



 A97: j in ( Seg n) by A66, A67, FINSEQ_1: 1;



 A98: ( len ( Col (P0,j))) = ( len P0) by MATRIX_0:def 8

 .= n by MATRIX_0: 24;

 ( len (( - (((a " ) * (A * (1,j))) * ( Base_FinSeq (K,n,1)))) + ( Base_FinSeq (K,n,j)))) = n by A70, A68, Th2;

 then

 A99: ( Col (P0,j)) = (( - (((a " ) * (A * (1,j))) * ( Base_FinSeq (K,n,1)))) + ( Base_FinSeq (K,n,j))) by A98, A72, FINSEQ_1: 14;



 A100: (( Line (A,1)) /. j) = (( Line (A,1)) . j) by A66, A67, A95, FINSEQ_4: 15

 .= (A * (1,j)) by A97, A94, MATRIX_0:def 7;

 [1, j] in ( Indices (A * P0)) by A9, A66, A67, MATRIX_0: 31;



 then ((A * P0) * (1,j)) = |(( Line (A,1)), ( Col (P0,j)))| by A23, A94, MATRIX_3:def 4

 .= ( |(( Line (A,1)), ( - (((a " ) * (A * (1,j))) * ( Base_FinSeq (K,n,1)))))| + |(( Line (A,1)), ( Base_FinSeq (K,n,j)))|) by A42, A70, A68, A99, Th11

 .= ( |(( Line (A,1)), (( - ((a " ) * (A * (1,j)))) * ( Base_FinSeq (K,n,1))))| + |(( Line (A,1)), ( Base_FinSeq (K,n,j)))|) by Th6

 .= ((( - ((a " ) * (A * (1,j)))) * |(( Line (A,1)), ( Base_FinSeq (K,n,1)))|) + |(( Line (A,1)), ( Base_FinSeq (K,n,j)))|) by A42, A19, Th10

 .= ((( - ((a " ) * (A * (1,j)))) * a) + |(( Line (A,1)), ( Base_FinSeq (K,n,j)))|) by A42, A3, A96, Th35

 .= (( - (((a " ) * (A * (1,j))) * a)) + |(( Line (A,1)), ( Base_FinSeq (K,n,j)))|) by VECTSP_1: 9

 .= (( - ((A * (1,j)) * ((a " ) * a))) + |(( Line (A,1)), ( Base_FinSeq (K,n,j)))|) by GROUP_1:def 3

 .= (( - ((A * (1,j)) * ( 1. K))) + |(( Line (A,1)), ( Base_FinSeq (K,n,j)))|) by A2, VECTSP_1:def 10

 .= (( - ((A * (1,j)) * ( 1. K))) + (( Line (A,1)) /. j)) by A42, A66, A67, Th35

 .= (( - (A * (1,j))) + (A * (1,j))) by A100

 .= ( 0. K) by RLVECT_1: 5;

 hence thesis;

 end;



 A101: ( Indices A) = [:( Seg n), ( Seg n):] & ( Indices (A * P0)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;



 A102: ( len ( Col (P0,1))) = ( len P0) by MATRIX_0:def 8

 .= n by MATRIX_0: 24;

 ( len ((a " ) * ( Base_FinSeq (K,n,1)))) = ( len ( Base_FinSeq (K,n,1))) by MATRIXR1: 16

 .= n by Th23;

 then

 A103: ( Col (P0,1)) = ((a " ) * ( Base_FinSeq (K,n,1))) by A102, A25, FINSEQ_1: 14;



 A104: ( len ((a " ) * ( Line (A,1)))) = ( len ( Line (A,1))) by MATRIXR1: 16

 .= n by A41, MATRIX_0:def 7;

 [1, 1] in ( Indices A) by A3, MATRIX_0: 31;



 then ((A * P0) * (1,1)) = |(( Line (A,1)), ( Col (P0,1)))| by A23, A41, A101, MATRIX_3:def 4

 .= ((a " ) * |(( Line (A,1)), ( Base_FinSeq (K,n,1)))|) by A42, A19, A103, Th10

 .= ((a " ) * (( Line (A,1)) /. 1)) by A42, A3, Th35

 .= (((a " ) * ( Line (A,1))) /. 1) by A43, POLYNOM1:def 1

 .= (((a " ) * ( Line (A,1))) . 1) by A3, A104, FINSEQ_4: 15

 .= ((a " ) * (A * (1,1))) by A44, A40, MATRIX12: 3

 .= ( 1. K) by A2, VECTSP_1:def 10;

 hence thesis by A22, A65, A45;

 end;

 theorem :: MATRIX14:40



 Th40: for A be Matrix of n, K st n > 0 & (A * (1,1)) <> ( 0. K) holds ex P be Matrix of n, K st P is invertible & ((P * A) * (1,1)) = ( 1. K) & (for i st 1 < i & i <= n holds ((P * A) * (i,1)) = ( 0. K)) & for j st 1 < j & j <= n & (A * (1,j)) = ( 0. K) holds ((P * A) * (1,j)) = ( 0. K)

 proof

 let A be Matrix of n, K;

 assume that

 A1: n > 0 and

 A2: (A * (1,1)) <> ( 0. K);

 set B = (A @ );



 A3: ( 0 + 1) <= n by A1, NAT_1: 13;

 then [1, 1] in ( Indices A) by MATRIX_0: 31;

 then (B * (1,1)) = (A * (1,1)) by MATRIX_0:def 6;

 then

 consider P0 be Matrix of n, K such that

 A4: P0 is invertible and

 A5: ((B * P0) * (1,1)) = ( 1. K) and

 A6: for i st 1 < i & i <= n holds ((B * P0) * (1,i)) = ( 0. K) and

 A7: for j st 1 < j & j <= n & (B * (j,1)) = ( 0. K) holds ((B * P0) * (j,1)) = ( 0. K) by A1, A2, Th39;



 A8: [1, 1] in ( Indices (B * P0)) by A3, MATRIX_0: 31;



 A9: for j st 1 < j & j <= n & (A * (1,j)) = ( 0. K) holds (((P0 @ ) * A) * (1,j)) = ( 0. K)

 proof

 let j;

 assume that

 A10: 1 < j & j <= n and

 A11: (A * (1,j)) = ( 0. K);

 [1, j] in ( Indices A) by A3, A10, MATRIX_0: 31;

 then (B * (j,1)) = (A * (1,j)) by MATRIX_0:def 6;

 then

 A12: ((B * P0) * (j,1)) = ( 0. K) by A7, A10, A11;

 [j, 1] in ( Indices (B * P0)) by A3, A10, MATRIX_0: 31;

 then (((B * P0) @ ) * (1,j)) = ( 0. K) by A12, MATRIX_0:def 6;

 then (((P0 @ ) * (B @ )) * (1,j)) = ( 0. K) by Th30;

 hence thesis by MATRIXR2: 29;

 end;



 A13: for i st 1 < i & i <= n holds (((P0 @ ) * A) * (i,1)) = ( 0. K)

 proof

 let i;

 assume 1 < i & i <= n;

 then

 A14: [1, i] in ( Indices (B * P0)) & ((B * P0) * (1,i)) = ( 0. K) by A3, A6, MATRIX_0: 31;

 ((B * P0) @ ) = ((P0 @ ) * (B @ )) by Th30

 .= ((P0 @ ) * A) by MATRIXR2: 29;

 hence thesis by A14, MATRIX_0:def 6;

 end;



 A15: (P0 @ ) is invertible by A4;

 (((P0 @ ) * A) * (1,1)) = (((P0 @ ) * (B @ )) * (1,1)) by MATRIXR2: 29

 .= (((B * P0) @ ) * (1,1)) by Th30

 .= ( 1. K) by A5, A8, MATRIX_0:def 6;

 hence thesis by A13, A15, A9;

 end;

 theorem :: MATRIX14:41



 Th41: for A be Matrix of n, K st n > 0 & (A * (1,1)) <> ( 0. K) holds ex P,Q be Matrix of n, K st P is invertible & Q is invertible & (((P * A) * Q) * (1,1)) = ( 1. K) & (for i st 1 0 and

 A2: (A * (1,1)) <> ( 0. K);

 consider P be Matrix of n, K such that

 A3: P is invertible and

 A4: ((P * A) * (1,1)) = ( 1. K) and

 A5: for i st 1 < i & i <= n holds ((P * A) * (i,1)) = ( 0. K) and for j st 1 < j & j <= n & (A * (1,j)) = ( 0. K) holds ((P * A) * (1,j)) = ( 0. K) by A1, A2, Th40;

 consider Q be Matrix of n, K such that

 A6: Q is invertible & (((P * A) * Q) * (1,1)) = ( 1. K) & for j st 1 < j & j <= n holds (((P * A) * Q) * (1,j)) = ( 0. K) and

 A7: for i st 1 < i & i <= n & ((P * A) * (i,1)) = ( 0. K) holds (((P * A) * Q) * (i,1)) = ( 0. K) by A1, A4, Th39;

 for i st 1 < i & i <= n holds (((P * A) * Q) * (i,1)) = ( 0. K)

 proof

 let i;

 assume

 A8: 1 < i & i <= n;

 then ((P * A) * (i,1)) = ( 0. K) by A5;

 hence thesis by A7, A8;

 end;

 hence thesis by A3, A6;

 end;

 begin

 theorem :: MATRIX14:42



 Th42: for D be non empty set, m,n,i,j be Element of NAT , A be Matrix of m, n, D holds ( Swap (A,i,j)) is Matrix of m, n, D

 proof

 let D be non empty set, m,n,i,j be Element of NAT , A be Matrix of m, n, D;



 A1: for p be FinSequence of D st p in ( rng ( Swap (A,i,j))) holds ( len p) = n

 proof

 let p be FinSequence of D;



 A2: ( rng ( Swap (A,i,j))) = ( rng A) by FINSEQ_7: 22;

 assume p in ( rng ( Swap (A,i,j)));

 hence thesis by A2, MATRIX_0:def 2;

 end;

 ( rng ( Swap (A,i,j))) = ( rng A) by FINSEQ_7: 22;

 then ex n3 be Nat st for x be object st x in ( rng ( Swap (A,i,j))) holds ex p be FinSequence of D st x = p & ( len p) = n3 by MATRIX_0: 9;

 then

 A3: ( Swap (A,i,j)) is Matrix of D by MATRIX_0: 9;

 ( len A) = m & ( len ( Swap (A,i,j))) = ( len A) by FINSEQ_7: 18, MATRIX_0:def 2;

 hence thesis by A3, A1, MATRIX_0:def 2;

 end;

 definition

 let K;

 let n be Element of NAT , i0 be Nat;

 :: MATRIX14:def3

 func SwapDiagonal (K,n,i0) -> Matrix of n, K equals ( Swap (( 1. (K,n)),1,i0));

 correctness

 proof

 i0 in NAT by ORDINAL1:def 12;

 hence thesis by Th42;

 end;

 end

 theorem :: MATRIX14:43



 Th43: for n be Element of NAT , i0 be Nat, A be Matrix of n, K st 1 <= i0 & i0 <= n & A = ( SwapDiagonal (K,n,i0)) holds for i,j be Nat st 1 <= i & i <= n & 1 <= j & j <= n holds (i0 <> 1 implies (i = 1 & j = i0 implies (A * (i,j)) = ( 1. K)) & (i = i0 & j = 1 implies (A * (i,j)) = ( 1. K)) & (i = 1 & j = 1 implies (A * (i,j)) = ( 0. K)) & (i = i0 & j = i0 implies (A * (i,j)) = ( 0. K)) & ( not ((i = 1 or i = i0) & (j = 1 or j = i0)) implies (i = j implies (A * (i,j)) = ( 1. K)) & (i <> j implies (A * (i,j)) = ( 0. K))))

 proof

 let n be Element of NAT , i0 be Nat, A be Matrix of n, K;

 assume

 A1: 1 <= i0 & i0 <= n;

 assume

 A2: A = ( SwapDiagonal (K,n,i0));

 let i,j be Nat;

 assume that

 A3: 1 <= i and

 A4: i <= n and

 A5: 1 <= j and

 A6: j <= n;



 A7: [i, j] in ( Indices A) by A3, A4, A5, A6, MATRIX_0: 31;

 assume

 A8: i0 <> 1;

 thus i = 1 & j = i0 implies (A * (i,j)) = ( 1. K)

 proof

 reconsider j0 = (i0 -' 2) as Element of NAT ;

 reconsider f = ( 1. (K,n)) as FinSequence of (the carrier of K * );

 assume that

 A9: i = 1 and

 A10: j = i0;

 reconsider qq = (f /. i0) as FinSequence of the carrier of K by FINSEQ_1:def 11;

 i0 <= ( len f) by A6, A10, MATRIX_0:def 2;



 then (f /. i0) = (f . i0) by A5, A10, FINSEQ_4: 15

 .= ( Base_FinSeq (K,n,i0)) by A5, A6, A10, Th26;

 then

 A11: (qq . j) = ( 1. K) by A5, A6, A10, Th24;

 reconsider g = (f /^ 1) as FinSequence of (the carrier of K * );



 A12: ( len f) = n by MATRIX_0:def 2;

 reconsider h = (g | j0) as FinSequence of (the carrier of K * );

 ( len ( <*(f /. i0)*> ^ h)) = (( len <*(f /. i0)*>) + ( len h)) by FINSEQ_1: 22

 .= (1 + ( len h)) by FINSEQ_1: 39;

 then

 A13: 1 <= ( len ( <*(f /. i0)*> ^ h)) by NAT_1: 11;



 A14: 1 = ( len <*(f /. i0)*>) by FINSEQ_1: 39;

 1 < i0 by A5, A8, A10, XXREAL_0: 1;



 then (A . i) = (((( <*(f /. i0)*> ^ h) ^ <*(f /. 1)*>) ^ (f /^ i0)) . i) by A2, A6, A10, A12, FINSEQ_7: 28

 .= ((( <*(f /. i0)*> ^ h) ^ ( <*(f /. 1)*> ^ (f /^ i0))) . i) by FINSEQ_1: 32

 .= (( <*(f /. i0)*> ^ h) . 1) by A9, A13, FINSEQ_1: 64

 .= ( <*(f /. i0)*> . 1) by A14, FINSEQ_1: 64

 .= (f /. i0) by FINSEQ_1:def 8;

 hence thesis by A7, A11, MATRIX_0:def 5;

 end;



 A15: ( len A) = n by MATRIX_0: 24;



 A16: 1 <= n by A3, A4, XXREAL_0: 2;

 thus i = i0 & j = 1 implies (A * (i,j)) = ( 1. K)

 proof

 reconsider f = ( 1. (K,n)) as FinSequence of (the carrier of K * );

 assume that

 A17: i = i0 and

 A18: j = 1;

 reconsider qq = (f /. 1) as FinSequence of the carrier of K by FINSEQ_1:def 11;



 A19: ( len f) = n by MATRIX_0:def 2;



 then (f /. 1) = (f . 1) by A16, FINSEQ_4: 15

 .= ( Base_FinSeq (K,n,1)) by A16, Th26;

 then

 A20: (qq . j) = ( 1. K) by A6, A18, Th24;

 (A . i) = (A /. i) by A15, A3, A4, FINSEQ_4: 15

 .= (f /. 1) by A2, A3, A4, A6, A17, A18, A19, FINSEQ_7: 31;

 hence thesis by A7, A20, MATRIX_0:def 5;

 end;

 thus i = 1 & j = 1 implies (A * (i,j)) = ( 0. K)

 proof

 reconsider f = ( 1. (K,n)) as FinSequence of (the carrier of K * );

 assume that

 A21: i = 1 and

 A22: j = 1;

 reconsider qq = (f /. i0) as FinSequence of the carrier of K by FINSEQ_1:def 11;



 A23: ( len f) = n by MATRIX_0:def 2;



 then (f /. i0) = (f . i0) by A1, FINSEQ_4: 15

 .= ( Base_FinSeq (K,n,i0)) by A1, Th26;

 then

 A24: (qq . j) = ( 0. K) by A4, A8, A21, A22, Th25;

 (A . i) = (A /. i) by A15, A3, A4, FINSEQ_4: 15

 .= (f /. i0) by A1, A2, A4, A21, A23, FINSEQ_7: 31;

 hence thesis by A7, A24, MATRIX_0:def 5;

 end;

 thus i = i0 & j = i0 implies (A * (i,j)) = ( 0. K)

 proof

 reconsider f = ( 1. (K,n)) as FinSequence of (the carrier of K * );

 assume that

 A25: i = i0 and

 A26: j = i0;

 reconsider qq = (f /. 1) as FinSequence of the carrier of K by FINSEQ_1:def 11;



 A27: ( len f) = n by MATRIX_0:def 2;



 then (f /. 1) = (f . 1) by A16, FINSEQ_4: 15

 .= ( Base_FinSeq (K,n,1)) by A16, Th26;

 then

 A28: (qq . j) = ( 0. K) by A1, A8, A26, Th25;

 (A . i) = (A /. i) by A15, A3, A4, FINSEQ_4: 15

 .= (f /. 1) by A2, A3, A4, A16, A25, A27, FINSEQ_7: 31;

 hence thesis by A7, A28, MATRIX_0:def 5;

 end;

 assume

 A29: not ((i = 1 or i = i0) & (j = 1 or j = i0));

 per cases by A29;

 suppose

 A30: i <> 1 & i <> i0;

 thus i = j implies (A * (i,j)) = ( 1. K)

 proof

 reconsider f = ( 1. (K,n)) as FinSequence of (the carrier of K * );

 assume

 A31: i = j;

 reconsider qq = (f /. i) as FinSequence of the carrier of K by FINSEQ_1:def 11;

 j <= ( len f) by A6, MATRIX_0:def 2;



 then (f /. i) = (f . i) by A5, A31, FINSEQ_4: 15

 .= ( Base_FinSeq (K,n,i)) by A3, A4, Th26;

 then

 A32: (qq . j) = ( 1. K) by A3, A4, A31, Th24;



 A33: ( len f) = n by MATRIX_0:def 2;

 (A . i) = (A /. i) by A15, A3, A4, FINSEQ_4: 15

 .= (f /. i) by A2, A3, A4, A30, A33, FINSEQ_7: 30;

 hence thesis by A7, A32, MATRIX_0:def 5;

 end;

 thus i <> j implies (A * (i,j)) = ( 0. K)

 proof

 reconsider f = ( 1. (K,n)) as FinSequence of (the carrier of K * );

 assume

 A34: i <> j;

 reconsider qq = (f /. i) as FinSequence of the carrier of K by FINSEQ_1:def 11;



 A35: ( len f) = n by MATRIX_0:def 2;



 then (f /. i) = (f . i) by A3, A4, FINSEQ_4: 15

 .= ( Base_FinSeq (K,n,i)) by A3, A4, Th26;

 then

 A36: (qq . j) = ( 0. K) by A5, A6, A34, Th25;

 (A . i) = (A /. i) by A15, A3, A4, FINSEQ_4: 15

 .= (f /. i) by A2, A3, A4, A30, A35, FINSEQ_7: 30;

 hence thesis by A7, A36, MATRIX_0:def 5;

 end;

 end;

 suppose

 A37: j <> 1 & j <> i0;

 thus i = j implies (A * (i,j)) = ( 1. K)

 proof

 reconsider f = ( 1. (K,n)) as FinSequence of (the carrier of K * );

 assume

 A38: i = j;

 reconsider qq = (f /. i) as FinSequence of the carrier of K by FINSEQ_1:def 11;

 j <= ( len f) by A6, MATRIX_0:def 2;



 then (f /. i) = (f . i) by A5, A38, FINSEQ_4: 15

 .= ( Base_FinSeq (K,n,i)) by A3, A4, Th26;

 then

 A39: (qq . j) = ( 1. K) by A3, A4, A38, Th24;



 A40: ( len f) = n by MATRIX_0:def 2;

 (A . i) = (A /. i) by A15, A3, A4, FINSEQ_4: 15

 .= (f /. i) by A2, A3, A4, A37, A38, A40, FINSEQ_7: 30;

 hence thesis by A7, A39, MATRIX_0:def 5;

 end;

 thus i <> j implies (A * (i,j)) = ( 0. K)

 proof

 assume

 A41: i <> j;

 per cases ;

 suppose

 A42: not (i = 1 or i = i0);

 reconsider f = ( 1. (K,n)) as FinSequence of (the carrier of K * );

 reconsider qq = (f /. i) as FinSequence of the carrier of K by FINSEQ_1:def 11;



 A43: ( len f) = n by MATRIX_0:def 2;



 then (f /. i) = (f . i) by A3, A4, FINSEQ_4: 15

 .= ( Base_FinSeq (K,n,i)) by A3, A4, Th26;

 then

 A44: (qq . j) = ( 0. K) by A5, A6, A41, Th25;

 (A . i) = (A /. i) by A15, A3, A4, FINSEQ_4: 15

 .= (f /. i) by A2, A3, A4, A42, A43, FINSEQ_7: 30;

 hence thesis by A7, A44, MATRIX_0:def 5;

 end;

 suppose

 A45: i = 1 or i = i0;

 per cases by A45;

 suppose

 A46: i = 1;

 reconsider f = ( 1. (K,n)) as FinSequence of (the carrier of K * );

 reconsider qq = (f /. i0) as FinSequence of the carrier of K by FINSEQ_1:def 11;



 A47: ( len f) = n by MATRIX_0:def 2;



 then (f /. i0) = (f . i0) by A1, FINSEQ_4: 15

 .= ( Base_FinSeq (K,n,i0)) by A1, Th26;

 then

 A48: (qq . j) = ( 0. K) by A5, A6, A37, Th25;

 (A . i) = (A /. i) by A15, A3, A4, FINSEQ_4: 15

 .= (f /. i0) by A1, A2, A4, A46, A47, FINSEQ_7: 31;

 hence thesis by A7, A48, MATRIX_0:def 5;

 end;

 suppose

 A49: i = i0;

 reconsider f = ( 1. (K,n)) as FinSequence of (the carrier of K * );

 reconsider qq = (f /. 1) as FinSequence of the carrier of K by FINSEQ_1:def 11;



 A50: ( len f) = n by MATRIX_0:def 2;



 then (f /. 1) = (f . 1) by A16, FINSEQ_4: 15

 .= ( Base_FinSeq (K,n,1)) by A16, Th26;

 then

 A51: (qq . j) = ( 0. K) by A5, A6, A37, Th25;

 (A . i) = (A /. i) by A15, A3, A4, FINSEQ_4: 15

 .= (f /. 1) by A2, A3, A4, A16, A49, A50, FINSEQ_7: 31;

 hence thesis by A7, A51, MATRIX_0:def 5;

 end;

 end;

 end;

 end;

 end;

 theorem :: MATRIX14:44



 Th44: for n be Element of NAT , A be Matrix of n, K holds for i be Nat st 1 <= i & i <= n holds (( SwapDiagonal (K,n,1)) * (i,i)) = ( 1. K)

 proof

 let n be Element of NAT , A be Matrix of n, K;

 set A = ( SwapDiagonal (K,n,1));

 let i be Nat;

 assume 1 <= i & i <= n;

 then A = ( 1. (K,n)) & [i, i] in ( Indices A) by FINSEQ_7: 19, MATRIX_0: 31;

 hence thesis by MATRIX_1:def 3;

 end;

 theorem :: MATRIX14:45



 Th45: for n be Element of NAT , A be Matrix of n, K holds for i,j be Nat st 1 <= i & i <= n & 1 <= j & j <= n holds (i <> j implies (( SwapDiagonal (K,n,1)) * (i,j)) = ( 0. K))

 proof

 let n be Element of NAT , A be Matrix of n, K;

 set A = ( SwapDiagonal (K,n,1));

 let i,j be Nat;

 assume 1 <= i & i <= n & 1 <= j & j <= n;

 then

 A1: [i, j] in ( Indices A) by MATRIX_0: 31;

 A = ( 1. (K,n)) by FINSEQ_7: 19;

 hence thesis by A1, MATRIX_1:def 3;

 end;

 theorem :: MATRIX14:46



 Th46: for K holds for n,i0 be Element of NAT , A be Matrix of n, K st i0 = 1 & for i,j be Nat st 1 <= i & i <= n & 1 <= j & j <= n holds (i = j implies (A * (i,j)) = ( 1. K)) & (i <> j implies (A * (i,j)) = ( 0. K)) holds A = ( SwapDiagonal (K,n,i0))

 proof

 let K;

 let n,i0 be Element of NAT , A be Matrix of n, K;

 assume

 A1: i0 = 1;

 assume

 A2: for i,j be Nat st 1 <= i & i <= n & 1 <= j & j <= n holds (i = j implies (A * (i,j)) = ( 1. K)) & (i <> j implies (A * (i,j)) = ( 0. K));

 for i,j be Nat st [i, j] in ( Indices A) holds (A * (i,j)) = (( SwapDiagonal (K,n,i0)) * (i,j))

 proof

 let i,j be Nat;

 assume

 A3: [i, j] in ( Indices A);

 ( Indices A) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

 then i in ( Seg n) by A3, ZFMISC_1: 87;

 then

 A4: 1 <= i & i <= n by FINSEQ_1: 1;

 then

 A5: i = j implies (A * (i,j)) = ( 1. K) by A2;

 ( width A) = n by MATRIX_0: 24;

 then j in ( Seg n) by A3, ZFMISC_1: 87;

 then

 A6: 1 <= j & j <= n by FINSEQ_1: 1;

 then i <> j implies (A * (i,j)) = ( 0. K) by A2, A4;

 hence thesis by A1, A4, A6, A5, Th44, Th45;

 end;

 hence thesis by MATRIX_0: 27;

 end;

 theorem :: MATRIX14:47



 Th47: for K holds for n,i0 be Element of NAT , A be Matrix of n, K st 1 <= i0 & i0 <= n & i0 <> 1 & for i,j be Nat st 1 <= i & i <= n & 1 <= j & j <= n holds (i = 1 & j = i0 implies (A * (i,j)) = ( 1. K)) & (i = i0 & j = 1 implies (A * (i,j)) = ( 1. K)) & (i = 1 & j = 1 implies (A * (i,j)) = ( 0. K)) & (i = i0 & j = i0 implies (A * (i,j)) = ( 0. K)) & ( not ((i = 1 or i = i0) & (j = 1 or j = i0)) implies (i = j implies (A * (i,j)) = ( 1. K)) & (i <> j implies (A * (i,j)) = ( 0. K))) holds A = ( SwapDiagonal (K,n,i0))

 proof

 let K;

 let n,i0 be Element of NAT , A be Matrix of n, K;

 assume

 A1: 1 <= i0 & i0 <= n & i0 <> 1;

 assume

 A2: for i,j be Nat st 1 <= i & i <= n & 1 <= j & j <= n holds (i = 1 & j = i0 implies (A * (i,j)) = ( 1. K)) & (i = i0 & j = 1 implies (A * (i,j)) = ( 1. K)) & (i = 1 & j = 1 implies (A * (i,j)) = ( 0. K)) & (i = i0 & j = i0 implies (A * (i,j)) = ( 0. K)) & ( not ((i = 1 or i = i0) & (j = 1 or j = i0)) implies (i = j implies (A * (i,j)) = ( 1. K)) & (i <> j implies (A * (i,j)) = ( 0. K)));

 for i,j be Nat st [i, j] in ( Indices A) holds (A * (i,j)) = (( SwapDiagonal (K,n,i0)) * (i,j))

 proof

 let i,j be Nat;

 assume

 A3: [i, j] in ( Indices A);

 ( Indices A) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

 then

 A4: i in ( Seg n) by A3, ZFMISC_1: 87;

 then

 A5: 1 <= i by FINSEQ_1: 1;



 A6: i = i0 & j = i0 implies (( SwapDiagonal (K,n,i0)) * (i,j)) = ( 0. K) by A1, Th43;

 ( width A) = n by MATRIX_0: 24;

 then

 A7: j in ( Seg n) by A3, ZFMISC_1: 87;

 then

 A8: 1 <= j by FINSEQ_1: 1;



 A9: i <= n by A4, FINSEQ_1: 1;

 then

 A10: i = i0 & j = i0 implies (A * (i,j)) = ( 0. K) by A2, A5;



 A11: j <= n by A7, FINSEQ_1: 1;

 then

 A12: i = 1 & j = i0 implies (A * (i,j)) = ( 1. K) by A2, A9, A8;



 A13: i = 1 & j = 1 implies (( SwapDiagonal (K,n,i0)) * (i,j)) = ( 0. K) by A1, A9, Th43;



 A14: i = 1 & j = 1 implies (A * (i,j)) = ( 0. K) by A2, A9;



 A15: i = i0 & j = 1 implies (A * (i,j)) = ( 1. K) by A2, A5, A9, A11;

 not ((i = 1 or i = i0) & (j = 1 or j = i0)) implies (i = j implies (A * (i,j)) = ( 1. K)) & (i <> j implies (A * (i,j)) = ( 0. K)) by A2, A5, A9, A8, A11;

 hence thesis by A1, A5, A9, A8, A11, A12, A15, A14, A10, A13, A6, Th43;

 end;

 hence thesis by MATRIX_0: 27;

 end;

 theorem :: MATRIX14:48



 Th48: for A be Matrix of n, K, i0 be Element of NAT st 1 <= i0 & i0 <= n holds (for j st 1 <= j & j <= n holds ((( SwapDiagonal (K,n,i0)) * A) * (i0,j)) = (A * (1,j)) & ((( SwapDiagonal (K,n,i0)) * A) * (1,j)) = (A * (i0,j))) & (for i, j st i <> 1 & i <> i0 & 1 <= i & i <= n & 1 <= j & j <= n holds ((( SwapDiagonal (K,n,i0)) * A) * (i,j)) = (A * (i,j)))

 proof

 let A be Matrix of n, K, i0 be Element of NAT ;

 assume that

 A1: 1 <= i0 and

 A2: i0 <= n;

 thus for j st 1 <= j & j <= n holds ((( SwapDiagonal (K,n,i0)) * A) * (i0,j)) = (A * (1,j)) & ((( SwapDiagonal (K,n,i0)) * A) * (1,j)) = (A * (i0,j))

 proof

 set Q = ( SwapDiagonal (K,n,i0)), P = A;

 let j;



 A3: ( width Q) = n by MATRIX_0: 24;



 A4: 1 <= n by A1, A2, XXREAL_0: 2;



 A5: for j2 be Nat st j2 in ( Seg ( width Q)) holds (( Base_FinSeq (K,n,i0)) . j2) = (Q * (1,j2))

 proof

 let j2 be Nat;

 reconsider j3 = j2 as Element of NAT by ORDINAL1:def 12;

 assume

 A6: j2 in ( Seg ( width Q));

 then

 A7: 1 <= j2 by FINSEQ_1: 1;



 A8: j2 <= n by A3, A6, FINSEQ_1: 1;

 now

 per cases ;

 suppose

 A9: i0 <> 1;

 now

 per cases ;

 suppose i0 = 1 & j2 = i0;

 hence thesis by A9;

 end;

 suppose

 A10: i0 = i0 & j2 = 1;

 then (( SwapDiagonal (K,n,i0)) * (1,j3)) = ( 0. K) by A1, A2, A8, A9, Th43;

 hence thesis by A4, A9, A10, Th25;

 end;

 suppose i0 = 1 & j2 = 1;

 hence thesis by A9;

 end;

 suppose

 A11: i0 = i0 & j2 = i0;

 then (( SwapDiagonal (K,n,i0)) * (1,j3)) = ( 1. K) by A1, A2, A4, A9, Th43;

 hence thesis by A7, A8, A11, Th24;

 end;

 suppose

 A12: not ((i0 = 1 or i0 = i0) & (j2 = 1 or j2 = i0));

 now

 per cases ;

 suppose i0 = j2;

 hence thesis by A12;

 end;

 suppose

 A13: i0 <> j2;

 (( SwapDiagonal (K,n,i0)) * (1,j3)) = ( 0. K) by A1, A2, A4, A7, A8, A9, A12, Th43;

 hence thesis by A7, A8, A13, Th25;

 end;

 end;

 hence thesis;

 end;

 end;

 hence thesis;

 end;

 suppose

 A14: i0 = 1;

 now

 per cases ;

 suppose

 A15: i0 = j2;

 then (( SwapDiagonal (K,n,i0)) * (1,j3)) = ( 1. K) by A8, A14, Th44;

 hence thesis by A7, A8, A15, Th24;

 end;

 suppose

 A16: i0 <> j2;

 then (( SwapDiagonal (K,n,i0)) * (1,j3)) = ( 0. K) by A2, A7, A8, A14, Th45;

 hence thesis by A7, A8, A16, Th25;

 end;

 end;

 hence thesis;

 end;

 end;

 hence thesis;

 end;

 assume

 A17: 1 <= j & j <= n;

 then 1 <= n by XXREAL_0: 2;

 then

 A18: ( Indices (Q * P)) = [:( Seg n), ( Seg n):] & 1 in ( Seg n) by FINSEQ_1: 1, MATRIX_0: 24;



 A19: 1 <= n by A1, A2, XXREAL_0: 2;



 A20: for j2 be Nat st j2 in ( Seg ( width Q)) holds (( Base_FinSeq (K,n,1)) . j2) = (Q * (i0,j2))

 proof

 let j2 be Nat;

 reconsider j3 = j2 as Element of NAT by ORDINAL1:def 12;

 assume

 A21: j2 in ( Seg ( width Q));

 then

 A22: 1 <= j2 by FINSEQ_1: 1;



 A23: j2 <= n by A3, A21, FINSEQ_1: 1;

 now

 per cases ;

 suppose

 A24: i0 <> 1;

 now

 per cases ;

 suppose i0 = 1 & j2 = i0;

 hence thesis by A24;

 end;

 suppose

 A25: i0 = i0 & j2 = 1;

 then (( SwapDiagonal (K,n,i0)) * (i0,j3)) = ( 1. K) by A1, A2, A19, A24, Th43;

 hence thesis by A23, A25, Th24;

 end;

 suppose i0 = 1 & j2 = 1;

 hence thesis by A24;

 end;

 suppose

 A26: i0 = i0 & j2 = i0;

 then (( SwapDiagonal (K,n,i0)) * (i0,j3)) = ( 0. K) by A22, A23, A24, Th43;

 hence thesis by A1, A2, A24, A26, Th25;

 end;

 suppose

 A27: not ((i0 = 1 or i0 = i0) & (j2 = 1 or j2 = i0));

 now

 (( SwapDiagonal (K,n,i0)) * (i0,j3)) = ( 0. K) by A1, A2, A22, A23, A24, A27, Th43;

 hence thesis by A22, A23, A27, Th25;

 end;

 hence thesis;

 end;

 end;

 hence thesis;

 end;

 suppose

 A28: i0 = 1;

 now

 per cases ;

 suppose

 A29: i0 = j2;

 then (( SwapDiagonal (K,n,i0)) * (i0,j3)) = ( 1. K) by A23, A28, Th44;

 hence thesis by A23, A28, A29, Th24;

 end;

 suppose

 A30: i0 <> j2;

 then (( SwapDiagonal (K,n,1)) * (i0,j3)) = ( 0. K) by A1, A2, A22, A23, Th45;

 hence thesis by A22, A23, A28, A30, Th25;

 end;

 end;

 hence thesis;

 end;

 end;

 hence thesis;

 end;

 ( len ( Base_FinSeq (K,n,1))) = n by Th23

 .= ( width Q) by MATRIX_0: 24;

 then

 A31: ( Line (Q,i0)) = ( Base_FinSeq (K,n,1)) by A20, MATRIX_0:def 7;



 A32: ( len P) = n by MATRIX_0: 24;

 then

 A33: ( len ( Col (P,j))) = n by MATRIX_0:def 8;



 A34: 1 <= n by A17, XXREAL_0: 2;

 then 1 in ( Seg n) by FINSEQ_1: 1;

 then

 A35: 1 in ( dom P) by A32, FINSEQ_1:def 3;

 j in ( Seg n) by A17, FINSEQ_1: 1;

 then

 A36: [1, j] in ( Indices (Q * P)) by A18, ZFMISC_1: 87;

 [i0, j] in ( Indices (Q * P)) by A1, A2, A17, MATRIX_0: 31;



 hence ((( SwapDiagonal (K,n,i0)) * A) * (i0,j)) = |(( Base_FinSeq (K,n,1)), ( Col (P,j)))| by A3, A32, A31, MATRIX_3:def 4

 .= |(( Col (P,j)), ( Base_FinSeq (K,n,1)))| by FVSUM_1: 90

 .= (( Col (P,j)) . 1) by A34, A33, Th35

 .= (A * (1,j)) by A35, MATRIX_0:def 8;

 i0 in ( Seg n) by A1, A2, FINSEQ_1: 1;

 then

 A37: i0 in ( dom P) by A32, FINSEQ_1:def 3;

 ( len ( Base_FinSeq (K,n,i0))) = n by Th23

 .= ( width Q) by MATRIX_0: 24;

 then ( Line (Q,1)) = ( Base_FinSeq (K,n,i0)) by A5, MATRIX_0:def 7;



 hence ((( SwapDiagonal (K,n,i0)) * A) * (1,j)) = |(( Base_FinSeq (K,n,i0)), ( Col (P,j)))| by A3, A32, A36, MATRIX_3:def 4

 .= |(( Col (P,j)), ( Base_FinSeq (K,n,i0)))| by FVSUM_1: 90

 .= (( Col (P,j)) . i0) by A1, A2, A33, Th35

 .= (A * (i0,j)) by A37, MATRIX_0:def 8;

 end;

 thus for i, j st i <> 1 & i <> i0 & 1 <= i & i <= n & 1 <= j & j <= n holds ((( SwapDiagonal (K,n,i0)) * A) * (i,j)) = (A * (i,j))

 proof

 set Q = ( SwapDiagonal (K,n,i0)), P = A;

 let i, j;

 assume that

 A38: i <> 1 and

 A39: i <> i0 and

 A40: 1 <= i & i <= n and

 A41: 1 <= j & j <= n;



 A42: ( len P) = n by MATRIX_0: 24;

 then

 A43: ( len ( Col (P,j))) = n by MATRIX_0:def 8;



 A44: ( width Q) = n by MATRIX_0: 24;



 A45: for j2 be Nat st j2 in ( Seg ( width Q)) holds (( Base_FinSeq (K,n,i)) . j2) = (Q * (i,j2))

 proof

 let j2 be Nat;

 reconsider j3 = j2 as Element of NAT by ORDINAL1:def 12;

 assume j2 in ( Seg ( width Q));

 then

 A46: 1 <= j2 & j2 <= n by A44, FINSEQ_1: 1;

 now

 per cases ;

 suppose

 A47: i0 <> 1;

 now

 per cases ;

 suppose i = 1 & j2 = i0;

 hence thesis by A38;

 end;

 suppose i = i0 & j2 = 1;

 hence thesis by A39;

 end;

 suppose i = 1 & j2 = 1;

 hence thesis by A38;

 end;

 suppose i = i0 & j2 = i0;

 hence thesis by A39;

 end;

 suppose

 A48: not ((i = 1 or i = i0) & (j2 = 1 or j2 = i0));

 now

 per cases ;

 suppose

 A49: i = j2;

 then (( SwapDiagonal (K,n,i0)) * (i,j3)) = ( 1. K) by A1, A2, A46, A47, A48, Th43;

 hence thesis by A40, A49, Th24;

 end;

 suppose

 A50: i <> j2;

 then (( SwapDiagonal (K,n,i0)) * (i,j3)) = ( 0. K) by A1, A2, A38, A39, A40, A46, A47, Th43;

 hence thesis by A46, A50, Th25;

 end;

 end;

 hence thesis;

 end;

 end;

 hence thesis;

 end;

 suppose

 A51: i0 = 1;

 now

 per cases ;

 suppose

 A52: i = j2;

 then (( SwapDiagonal (K,n,i0)) * (i,j3)) = ( 1. K) by A46, A51, Th44;

 hence thesis by A46, A52, Th24;

 end;

 suppose

 A53: i <> j2;

 then (( SwapDiagonal (K,n,i0)) * (i,j3)) = ( 0. K) by A40, A46, A51, Th45;

 hence thesis by A46, A53, Th25;

 end;

 end;

 hence thesis;

 end;

 end;

 hence thesis;

 end;

 i in ( Seg n) by A40, FINSEQ_1: 1;

 then

 A54: i in ( dom P) by A42, FINSEQ_1:def 3;

 ( len ( Base_FinSeq (K,n,i))) = n by Th23

 .= ( width Q) by MATRIX_0: 24;

 then

 A55: ( Line (Q,i)) = ( Base_FinSeq (K,n,i)) by A45, MATRIX_0:def 7;

 [i, j] in ( Indices (Q * P)) by A40, A41, MATRIX_0: 31;



 hence ((( SwapDiagonal (K,n,i0)) * A) * (i,j)) = |(( Base_FinSeq (K,n,i)), ( Col (P,j)))| by A44, A42, A55, MATRIX_3:def 4

 .= |(( Col (P,j)), ( Base_FinSeq (K,n,i)))| by FVSUM_1: 90

 .= (( Col (P,j)) . i) by A40, A43, Th35

 .= (A * (i,j)) by A54, MATRIX_0:def 8;

 end;

 end;

 theorem :: MATRIX14:49



 Th49: for i0 be Element of NAT st 1 <= i0 & i0 <= n holds ( SwapDiagonal (K,n,i0)) is invertible & (( SwapDiagonal (K,n,i0)) ~ ) = ( SwapDiagonal (K,n,i0))

 proof

 let i0 be Element of NAT ;

 assume that

 A1: 1 <= i0 and

 A2: i0 <= n;



 A3: 1 <= n by A1, A2, XXREAL_0: 2;

 set R = (( SwapDiagonal (K,n,i0)) * ( SwapDiagonal (K,n,i0)));



 A4: ( Indices R) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;



 A5: ( width R) = n by MATRIX_0: 24;



 A6: for i4,j4 be Nat st [i4, j4] in ( Indices R) holds (R * (i4,j4)) = (( 1. (K,n)) * (i4,j4))

 proof

 let i4,j4 be Nat;

 reconsider i = i4, j = j4 as Element of NAT by ORDINAL1:def 12;

 assume

 A7: [i4, j4] in ( Indices R);

 then

 A8: [i, j] in ( Indices ( 1. (K,n))) by A4, MATRIX_0: 24;

 j in ( Seg n) by A5, A7, ZFMISC_1: 87;

 then

 A9: 1 <= j & j <= n by FINSEQ_1: 1;



 A10: i in ( Seg n) by A4, A7, ZFMISC_1: 87;

 then

 A11: 1 <= i by FINSEQ_1: 1;



 A12: i <= n by A10, FINSEQ_1: 1;

 per cases by A11, XXREAL_0: 1;

 suppose

 A13: 1 < i;

 now

 per cases ;

 suppose

 A14: i <> i0;

 now

 per cases ;

 suppose

 A15: i = j;

 A16:

 now

 per cases ;

 suppose i0 <> 1;

 hence (( SwapDiagonal (K,n,i0)) * (i,j)) = ( 1. K) by A1, A2, A12, A13, A14, A15, Th43;

 end;

 suppose i0 = 1;

 hence (( SwapDiagonal (K,n,i0)) * (i,j)) = ( 1. K) by A11, A12, A15, Th44;

 end;

 end;

 (( 1. (K,n)) * (i,j)) = ( 1. K) by A8, A15, MATRIX_1:def 3;

 hence (R * (i,j)) = (( 1. (K,n)) * (i,j)) by A1, A2, A12, A9, A13, A14, A16, Th48;

 end;

 suppose

 A17: i <> j;

 A18:

 now

 per cases ;

 suppose i0 = 1;

 hence (( SwapDiagonal (K,n,i0)) * (i,j)) = ( 0. K) by A11, A12, A9, A17, Th45;

 end;

 suppose i0 <> 1;

 hence (( SwapDiagonal (K,n,i0)) * (i,j)) = ( 0. K) by A1, A2, A12, A9, A13, A14, A17, Th43;

 end;

 end;

 (( 1. (K,n)) * (i,j)) = ( 0. K) by A8, A17, MATRIX_1:def 3;

 hence (R * (i,j)) = (( 1. (K,n)) * (i,j)) by A1, A2, A12, A9, A13, A14, A18, Th48;

 end;

 end;

 hence (R * (i,j)) = (( 1. (K,n)) * (i,j));

 end;

 suppose

 A19: i = i0;

 now

 per cases ;

 suppose

 A20: i = j;

 A21:

 now

 per cases ;

 suppose i0 = 1;

 hence (( SwapDiagonal (K,n,i0)) * (1,i0)) = ( 1. K) by A13, A19;

 end;

 suppose i0 <> 1;

 hence (( SwapDiagonal (K,n,i0)) * (1,i0)) = ( 1. K) by A1, A2, A3, Th43;

 end;

 end;

 (( 1. (K,n)) * (i,j)) = ( 1. K) by A8, A20, MATRIX_1:def 3;

 hence (R * (i,j)) = (( 1. (K,n)) * (i,j)) by A1, A2, A19, A20, A21, Th48;

 end;

 suppose

 A22: i <> j;

 A23:

 now

 now

 per cases ;

 suppose j = 1;

 hence (( SwapDiagonal (K,n,i0)) * (1,j)) = ( 0. K) by A2, A3, A13, A19, Th43;

 end;

 suppose j <> 1;

 hence (( SwapDiagonal (K,n,i0)) * (1,j)) = ( 0. K) by A3, A12, A9, A13, A19, A22, Th43;

 end;

 end;

 hence (( SwapDiagonal (K,n,i0)) * (1,j)) = ( 0. K);

 end;

 (( 1. (K,n)) * (i,j)) = ( 0. K) by A8, A22, MATRIX_1:def 3;

 hence (R * (i,j)) = (( 1. (K,n)) * (i,j)) by A11, A12, A9, A19, A23, Th48;

 end;

 end;

 hence (R * (i,j)) = (( 1. (K,n)) * (i,j));

 end;

 end;

 hence thesis;

 end;

 suppose

 A24: 1 = i;

 now

 per cases ;

 suppose

 A25: i0 <> 1;

 per cases ;

 suppose

 A26: j <> 1;

 A27:

 now

 per cases ;

 suppose j = i0;

 hence (( SwapDiagonal (K,n,i0)) * (i0,j)) = ( 0. K) by A9, A26, Th43;

 end;

 suppose j <> i0;

 hence (( SwapDiagonal (K,n,i0)) * (i0,j)) = ( 0. K) by A1, A2, A9, A25, A26, Th43;

 end;

 end;

 (( 1. (K,n)) * (i,j)) = ( 0. K) by A8, A24, A26, MATRIX_1:def 3;

 hence (R * (i,j)) = (( 1. (K,n)) * (i,j)) by A1, A2, A9, A24, A27, Th48;

 end;

 suppose j = 1;

 then (( 1. (K,n)) * (i,j)) = ( 1. K) & (( SwapDiagonal (K,n,i0)) * (i0,j)) = ( 1. K) by A1, A2, A3, A8, A24, A25, Th43, MATRIX_1:def 3;

 hence (R * (i,j)) = (( 1. (K,n)) * (i,j)) by A1, A2, A9, A24, Th48;

 end;

 end;

 suppose

 A28: i0 = 1;

 now

 per cases ;

 suppose i <> j;

 then (( 1. (K,n)) * (i,j)) = ( 0. K) & (( SwapDiagonal (K,n,1)) * (1,j)) = ( 0. K) by A12, A9, A8, A24, Th45, MATRIX_1:def 3;

 hence (R * (i,j)) = (( 1. (K,n)) * (i,j)) by A12, A9, A24, A28, Th48;

 end;

 suppose

 A29: i = j;

 then

 A30: (( 1. (K,n)) * (j,j)) = ( 1. K) by A8, MATRIX_1:def 3;

 ((( SwapDiagonal (K,n,i0)) * ( SwapDiagonal (K,n,i0))) * (1,j)) = (( SwapDiagonal (K,n,i0)) * (i0,j)) by A1, A2, A9, Th48;

 hence (R * (i,j)) = (( 1. (K,n)) * (i,j)) by A2, A24, A28, A29, A30, Th44;

 end;

 end;

 hence (R * (i,j)) = (( 1. (K,n)) * (i,j));

 end;

 end;

 hence thesis;

 end;

 end;

 ( width ( 1. (K,n))) = n by MATRIX_0: 24;

 then

 A31: ( width R) = ( width ( 1. (K,n))) by MATRIX_0: 24;

 ( len ( 1. (K,n))) = n by MATRIX_0: 24;

 then ( len R) = ( len ( 1. (K,n))) by MATRIX_0: 24;

 then

 A32: (( SwapDiagonal (K,n,i0)) * ( SwapDiagonal (K,n,i0))) = ( 1. (K,n)) by A31, A6, MATRIX_0: 21;

 hence ( SwapDiagonal (K,n,i0)) is invertible by Th19;

 thus thesis by A32, Th18;

 end;

 theorem :: MATRIX14:50



 Th50: for i0 be Element of NAT st 1 <= i0 & i0 <= n holds (( SwapDiagonal (K,n,i0)) @ ) = ( SwapDiagonal (K,n,i0))

 proof

 let i0 be Element of NAT ;

 assume

 A1: 1 <= i0 & i0 <= n;

 per cases ;

 suppose

 A2: i0 <> 1;

 for i,j be Nat st 1 <= i & i <= n & 1 <= j & j <= n holds (i = 1 & j = i0 implies ((( SwapDiagonal (K,n,i0)) @ ) * (i,j)) = ( 1. K)) & (i = i0 & j = 1 implies ((( SwapDiagonal (K,n,i0)) @ ) * (i,j)) = ( 1. K)) & (i = 1 & j = 1 implies ((( SwapDiagonal (K,n,i0)) @ ) * (i,j)) = ( 0. K)) & (i = i0 & j = i0 implies ((( SwapDiagonal (K,n,i0)) @ ) * (i,j)) = ( 0. K)) & ( not ((i = 1 or i = i0) & (j = 1 or j = i0)) implies (i = j implies ((( SwapDiagonal (K,n,i0)) @ ) * (i,j)) = ( 1. K)) & (i <> j implies ((( SwapDiagonal (K,n,i0)) @ ) * (i,j)) = ( 0. K)))

 proof



 A3: ( Indices ( SwapDiagonal (K,n,i0))) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

 let i,j be Nat;

 assume that

 A4: 1 <= i and

 A5: i <= n and

 A6: 1 <= j and

 A7: j <= n;



 A8: i in ( Seg n) & j in ( Seg n) by A4, A5, A6, A7, FINSEQ_1: 1;

 hereby

 assume

 A9: i = 1 & j = i0;

 [j, i] in ( Indices ( SwapDiagonal (K,n,i0))) by A8, A3, ZFMISC_1: 87;



 hence ((( SwapDiagonal (K,n,i0)) @ ) * (i,j)) = (( SwapDiagonal (K,n,i0)) * (j,i)) by MATRIX_0:def 6

 .= ( 1. K) by A2, A5, A6, A7, A9, Th43;

 end;

 hereby

 assume

 A10: i = i0 & j = 1;

 [j, i] in ( Indices ( SwapDiagonal (K,n,i0))) by A8, A3, ZFMISC_1: 87;



 hence ((( SwapDiagonal (K,n,i0)) @ ) * (i,j)) = (( SwapDiagonal (K,n,i0)) * (j,i)) by MATRIX_0:def 6

 .= ( 1. K) by A2, A4, A5, A7, A10, Th43;

 end;

 hereby

 assume

 A11: i = 1 & j = 1;

 [j, i] in ( Indices ( SwapDiagonal (K,n,i0))) by A8, A3, ZFMISC_1: 87;



 hence ((( SwapDiagonal (K,n,i0)) @ ) * (i,j)) = (( SwapDiagonal (K,n,i0)) * (j,i)) by MATRIX_0:def 6

 .= ( 0. K) by A1, A2, A5, A11, Th43;

 end;

 hereby

 assume

 A12: i = i0 & j = i0;

 [j, i] in ( Indices ( SwapDiagonal (K,n,i0))) by A8, A3, ZFMISC_1: 87;



 hence ((( SwapDiagonal (K,n,i0)) @ ) * (i,j)) = (( SwapDiagonal (K,n,i0)) * (j,i)) by MATRIX_0:def 6

 .= ( 0. K) by A2, A4, A5, A12, Th43;

 end;

 hereby

 assume

 A13: not ((i = 1 or i = i0) & (j = 1 or j = i0));



 A14: [j, i] in ( Indices ( SwapDiagonal (K,n,i0))) by A8, A3, ZFMISC_1: 87;

 A15:

 now

 assume

 A16: i = j;



 thus ((( SwapDiagonal (K,n,i0)) @ ) * (i,j)) = (( SwapDiagonal (K,n,i0)) * (j,i)) by A14, MATRIX_0:def 6

 .= ( 1. K) by A1, A2, A4, A5, A13, A16, Th43;

 end;

 now

 assume

 A17: i <> j;



 thus ((( SwapDiagonal (K,n,i0)) @ ) * (i,j)) = (( SwapDiagonal (K,n,i0)) * (j,i)) by A14, MATRIX_0:def 6

 .= ( 0. K) by A1, A2, A4, A5, A6, A7, A13, A17, Th43;

 end;

 hence (i = j implies ((( SwapDiagonal (K,n,i0)) @ ) * (i,j)) = ( 1. K)) & (i <> j implies ((( SwapDiagonal (K,n,i0)) @ ) * (i,j)) = ( 0. K)) by A15;

 end;

 end;

 hence thesis by A1, A2, Th47;

 end;

 suppose

 A18: i0 = 1;

 for i,j be Nat st 1 <= i & i <= n & 1 <= j & j <= n holds (i = j implies ((( SwapDiagonal (K,n,i0)) @ ) * (i,j)) = ( 1. K)) & (i <> j implies ((( SwapDiagonal (K,n,i0)) @ ) * (i,j)) = ( 0. K))

 proof



 A19: ( Indices ( SwapDiagonal (K,n,i0))) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

 let i,j be Nat;

 assume that

 A20: 1 <= i & i <= n and

 A21: 1 <= j & j <= n;

 i in ( Seg n) & j in ( Seg n) by A20, A21, FINSEQ_1: 1;

 then

 A22: [j, i] in ( Indices ( SwapDiagonal (K,n,i0))) by A19, ZFMISC_1: 87;

 hereby

 assume

 A23: i = j;



 thus ((( SwapDiagonal (K,n,i0)) @ ) * (i,j)) = (( SwapDiagonal (K,n,i0)) * (j,i)) by A22, MATRIX_0:def 6

 .= ( 1. K) by A18, A20, A23, Th44;

 end;

 hereby

 assume

 A24: i <> j;



 thus ((( SwapDiagonal (K,n,i0)) @ ) * (i,j)) = (( SwapDiagonal (K,n,i0)) * (j,i)) by A22, MATRIX_0:def 6

 .= ( 0. K) by A18, A20, A21, A24, Th45;

 end;

 end;

 hence thesis by A18, Th46;

 end;

 end;

 theorem :: MATRIX14:51



 Th51: for A be Matrix of n, K, j0 be Element of NAT st 1 <= j0 & j0 <= n holds (for i st 1 <= i & i <= n holds ((A * ( SwapDiagonal (K,n,j0))) * (i,j0)) = (A * (i,1)) & ((A * ( SwapDiagonal (K,n,j0))) * (i,1)) = (A * (i,j0))) & (for i, j st j <> 1 & j <> j0 & 1 <= i & i <= n & 1 <= j & j <= n holds ((A * ( SwapDiagonal (K,n,j0))) * (i,j)) = (A * (i,j)))

 proof

 let A be Matrix of n, K, j0 be Element of NAT ;

 assume

 A1: 1 <= j0 & j0 <= n;



 A2: ((( SwapDiagonal (K,n,j0)) * (A @ )) @ ) = (((A @ ) @ ) * (( SwapDiagonal (K,n,j0)) @ )) by Th30

 .= (A * (( SwapDiagonal (K,n,j0)) @ )) by MATRIXR2: 29

 .= (A * ( SwapDiagonal (K,n,j0))) by A1, Th50;



 A3: for i st 1 <= i & i <= n holds ((A * ( SwapDiagonal (K,n,j0))) * (i,j0)) = (A * (i,1)) & ((A * ( SwapDiagonal (K,n,j0))) * (i,1)) = (A * (i,j0))

 proof

 let i;

 assume

 A4: 1 <= i & i <= n;

 then

 A5: 1 <= n by XXREAL_0: 2;

 then

 A6: [i, 1] in ( Indices A) by A4, MATRIX_0: 31;

 [j0, i] in ( Indices (( SwapDiagonal (K,n,j0)) * (A @ ))) by A1, A4, MATRIX_0: 31;



 hence ((A * ( SwapDiagonal (K,n,j0))) * (i,j0)) = ((( SwapDiagonal (K,n,j0)) * (A @ )) * (j0,i)) by A2, MATRIX_0:def 6

 .= ((A @ ) * (1,i)) by A1, A4, Th48

 .= (A * (i,1)) by A6, MATRIX_0:def 6;



 A7: [i, j0] in ( Indices A) by A1, A4, MATRIX_0: 31;

 [1, i] in ( Indices (( SwapDiagonal (K,n,j0)) * (A @ ))) by A4, A5, MATRIX_0: 31;



 hence ((A * ( SwapDiagonal (K,n,j0))) * (i,1)) = ((( SwapDiagonal (K,n,j0)) * (A @ )) * (1,i)) by A2, MATRIX_0:def 6

 .= ((A @ ) * (j0,i)) by A1, A4, Th48

 .= (A * (i,j0)) by A7, MATRIX_0:def 6;

 end;

 for i, j st j <> 1 & j <> j0 & 1 <= i & i <= n & 1 <= j & j <= n holds ((A * ( SwapDiagonal (K,n,j0))) * (i,j)) = (A * (i,j))

 proof

 let i, j;

 assume that

 A8: j <> 1 & j <> j0 and

 A9: 1 <= i & i <= n & 1 <= j & j <= n;



 A10: [i, j] in ( Indices A) by A9, MATRIX_0: 31;

 [j, i] in ( Indices (( SwapDiagonal (K,n,j0)) * (A @ ))) by A9, MATRIX_0: 31;



 hence ((A * ( SwapDiagonal (K,n,j0))) * (i,j)) = ((( SwapDiagonal (K,n,j0)) * (A @ )) * (j,i)) by A2, MATRIX_0:def 6

 .= ((A @ ) * (j,i)) by A1, A8, A9, Th48

 .= (A * (i,j)) by A10, MATRIX_0:def 6;

 end;

 hence thesis by A3;

 end;

 theorem :: MATRIX14:52



 Th52: for A be Matrix of n, K holds A = ( 0. (K,n)) iff for i, j st 1 <= i & i <= n & 1 <= j & j <= n holds (A * (i,j)) = ( 0. K)

 proof

 let A be Matrix of n, K;



 A1: ( width A) = n by MATRIX_0: 24;

 thus A = ( 0. (K,n)) implies for i, j st 1 <= i & i <= n & 1 <= j & j <= n holds (A * (i,j)) = ( 0. K)

 proof

 assume A = ( 0. (K,n));

 then

 A2: A = ( 0. (K,n,n)) by MATRIX_3:def 1;

 thus for i, j st 1 <= i & i <= n & 1 <= j & j <= n holds (A * (i,j)) = ( 0. K)

 proof

 let i, j;

 assume 1 <= i & i <= n & 1 <= j & j <= n;

 then [i, j] in ( Indices A) by MATRIX_0: 31;

 hence thesis by A2, MATRIX_3: 1;

 end;

 end;

 assume

 A3: for i, j st 1 <= i & i <= n & 1 <= j & j <= n holds (A * (i,j)) = ( 0. K);



 A4: ( Indices A) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;



 A5: for i,j be Nat st [i, j] in ( Indices A) holds (A * (i,j)) = ((A + A) * (i,j))

 proof

 let i,j be Nat;

 reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def 12;

 assume

 A6: [i, j] in ( Indices A);

 then j in ( Seg n) by A1, ZFMISC_1: 87;

 then

 A7: 1 <= j & j <= n by FINSEQ_1: 1;

 i in ( Seg n) by A4, A6, ZFMISC_1: 87;

 then 1 <= i & i <= n by FINSEQ_1: 1;

 then (A * (i0,j0)) = ( 0. K) by A3, A7;



 then ((A + A) * (i,j)) = (( 0. K) + (A * (i,j))) by A6, MATRIX_3:def 3

 .= (A * (i,j)) by RLVECT_1: 4;

 hence thesis;

 end;

 ( len A) = n by MATRIX_0: 24;

 then A = ( 0. (K,n,n)) by A1, A5, MATRIX_0: 27, MATRIX_4: 6;

 hence thesis by MATRIX_3:def 1;

 end;

 begin

 theorem :: MATRIX14:53



 Th53: for A be Matrix of n, K st A <> ( 0. (K,n)) holds ex B,C be Matrix of n, K st B is invertible & C is invertible & (((B * A) * C) * (1,1)) = ( 1. K) & (for i st 1 ( 0. (K,n));

 then

 consider i0,j0 be Element of NAT such that

 A1: 1 <= i0 & i0 <= n and

 A2: 1 <= j0 & j0 <= n and

 A3: (A * (i0,j0)) <> ( 0. K) by Th52;

 set A3 = ((( SwapDiagonal (K,n,i0)) * A) * ( SwapDiagonal (K,n,j0)));

 set A2 = (( SwapDiagonal (K,n,i0)) * A);

 1 <= n by A1, XXREAL_0: 2;



 then (((( SwapDiagonal (K,n,i0)) * A) * ( SwapDiagonal (K,n,j0))) * (1,1)) = (A2 * (1,j0)) by A2, Th51

 .= (A * (i0,j0)) by A1, A2, Th48;

 then

 consider P,Q be Matrix of n, K such that

 A4: P is invertible and

 A5: Q is invertible and

 A6: ((((P * A3) * Q) * (1,1)) = ( 1. K) & for i st 1 < i & i <= n holds (((P * A3) * Q) * (i,1)) = ( 0. K)) & for j st 1 < j & j <= n holds (((P * A3) * Q) * (1,j)) = ( 0. K) by A1, A3, Th41;

 set B0 = (P * ( SwapDiagonal (K,n,i0))), C0 = (( SwapDiagonal (K,n,j0)) * Q);

 ( SwapDiagonal (K,n,i0)) is invertible by A1, Th49;

 then

 A7: B0 is invertible by A4, MATRIX_6: 36;

 ( SwapDiagonal (K,n,j0)) is invertible by A2, Th49;

 then

 A8: C0 is invertible by A5, MATRIX_6: 36;

 ((B0 * A) * C0) = ((P * (( SwapDiagonal (K,n,i0)) * A)) * (( SwapDiagonal (K,n,j0)) * Q)) by Th17

 .= (((P * (( SwapDiagonal (K,n,i0)) * A)) * ( SwapDiagonal (K,n,j0))) * Q) by Th17

 .= ((P * A3) * Q) by Th17;

 hence thesis by A6, A7, A8;

 end;

 theorem :: MATRIX14:54



 Th54: for A,B be Matrix of n, K st (B * A) = ( 1. (K,n)) holds ex B2 be Matrix of n, K st (A * B2) = ( 1. (K,n))

 proof

 let A,B be Matrix of n, K;

 thus (B * A) = ( 1. (K,n)) implies ex B2 be Matrix of n, K st (A * B2) = ( 1. (K,n))

 proof

 defpred P[ Nat] means for D,B3 be Matrix of $1, K st (B3 * D) = ( 1. (K,$1)) holds ex B4 be Matrix of $1, K st (D * B4) = ( 1. (K,$1));

 assume

 A1: (B * A) = ( 1. (K,n));



 A2: for k be Nat st P[k] holds P[(k + 1)]

 proof

 let k be Nat;

 assume

 A3: P[k];

 for A2,B3 be Matrix of (k + 1), K st (B3 * A2) = ( 1. (K,(k + 1))) holds ex B4 be Matrix of (k + 1), K st (A2 * B4) = ( 1. (K,(k + 1)))

 proof

 let A2,B2 be Matrix of (k + 1), K;



 A4: ( Indices ( 1. (K,(k + 1)))) = [:( Seg (k + 1)), ( Seg (k + 1)):] by MATRIX_0: 24;

 assume

 A5: (B2 * A2) = ( 1. (K,(k + 1)));

 then

 A6: (( Det B2) * ( Det A2)) = ( Det ( 1. (K,(k + 1)))) by MATRIXR2: 45;

 now

 assume A2 = ( 0. (K,(k + 1)));

 then A2 = ( 0. (K,(k + 1),(k + 1))) by MATRIX_3:def 1;

 then ( Det A2) = ( 0. K) by MATRIX_7: 15, NAT_1: 12;

 then

 A7: (( Det B2) * ( Det A2)) = ( 0. K);

 not ( 0. K) = ( 1_ K);

 hence contradiction by A6, A7, MATRIX_7: 16, NAT_1: 12;

 end;

 then

 consider B,C be Matrix of (k + 1), K such that

 A8: B is invertible and

 A9: C is invertible and

 A10: (((B * A2) * C) * (1,1)) = ( 1. K) and

 A11: for i st 1 < i & i <= (k + 1) holds (((B * A2) * C) * (i,1)) = ( 0. K) and

 A12: for j st 1 < j & j <= (k + 1) holds (((B * A2) * C) * (1,j)) = ( 0. K) by Th53;

 set A3 = ((B * A2) * C), B3 = (((C ~ ) * B2) * (B ~ ));



 A13: ( width B3) = (k + 1) by MATRIX_0: 24;



 A14: ( width A3) = (k + 1) by MATRIX_0: 24;



 A15: for j be Nat st 1 <= j & j <= ( len ( Line (A3,1))) holds (( Line (A3,1)) . j) = (( Base_FinSeq (K,(k + 1),1)) . j)

 proof

 let j be Nat;

 assume that

 A16: 1 <= j and

 A17: j <= ( len ( Line (A3,1)));



 A18: j <= (k + 1) by A14, A17, MATRIX_0:def 7;

 ( len ( Line (A3,1))) = ( width A3) by MATRIX_0:def 7;

 then

 A19: j in ( Seg ( width A3)) by A16, A17, FINSEQ_1: 1;

 per cases by A16, XXREAL_0: 1;

 suppose

 A20: 1 = j;

 then (( Line (A3,1)) . j) = ( 1. K) by A10, A19, MATRIX_0:def 7;

 hence thesis by A18, A20, Th24;

 end;

 suppose

 A21: 1 < j;



 A22: j in NAT by ORDINAL1:def 12;

 (( Line (A3,1)) . j) = (A3 * (1,j)) by A19, MATRIX_0:def 7

 .= ( 0. K) by A12, A18, A21, A22;

 hence thesis by A18, A21, Th25;

 end;

 end;



 A23: ( len <*( 0. K)*>) = 1 by FINSEQ_1: 40;

 deffunc f( Nat, Nat) = (A3 * (($1 + 1),($2 + 1)));



 A24: ( len (A2 * C)) = (k + 1) by MATRIX_0: 24;

 consider F be Matrix of k, k, K such that

 A25: for i,j be Nat st [i, j] in ( Indices F) holds (F * (i,j)) = f(i,j) from MATRIX_0:sch 1;



 A26: ( len F) = k by MATRIX_0: 24;

 deffunc g( Nat, Nat) = (B3 * (($1 + 1),($2 + 1)));



 A27: ( len C) = (k + 1) by MATRIX_0: 24;

 consider G be Matrix of k, k, K such that

 A28: for i,j be Nat st [i, j] in ( Indices G) holds (G * (i,j)) = g(i,j) from MATRIX_0:sch 1;



 A29: ( len A3) = (k + 1) by MATRIX_0: 24;



 A30: (B3 * A3) = ((((C ~ ) * B2) * (B ~ )) * (B * (A2 * C))) by Th17

 .= ((((( Inv C) * B2) * ( Inv B)) * B) * (A2 * C)) by Th17

 .= (((( Inv C) * B2) * (( Inv B) * B)) * (A2 * C)) by Th17

 .= (((( Inv C) * B2) * ( 1. (K,(k + 1)))) * (A2 * C)) by A8, Th18

 .= ((( Inv C) * B2) * (( 1. (K,(k + 1))) * (A2 * C))) by Th17

 .= ((( Inv C) * B2) * (A2 * C)) by A24, MATRIXR2: 68

 .= (((( Inv C) * B2) * A2) * C) by Th17

 .= ((( Inv C) * ( 1. (K,(k + 1)))) * C) by A5, Th17

 .= (( Inv C) * (( 1. (K,(k + 1))) * C)) by Th17

 .= (( Inv C) * C) by A27, MATRIXR2: 68

 .= ( 1. (K,(k + 1))) by A9, Th18;



 A31: for i be Nat st 1 < i & i <= (k + 1) holds (B3 * (i,1)) = (( 1. (K,(k + 1))) * (i,1))

 proof



 A32: ( len ( Base_FinSeq (K,(k + 1),1))) = (k + 1) by Th23;

 let i be Nat;



 A33: ( len ( Col (A3,1))) = ( len A3) by MATRIX_0:def 8

 .= (k + 1) by MATRIX_0: 24;



 A34: ( len A3) = (k + 1) by MATRIX_0: 24;



 A35: for k2 be Nat st 1 <= k2 & k2 <= ( len ( Col (A3,1))) holds (( Col (A3,1)) . k2) = (( Base_FinSeq (K,(k + 1),1)) . k2)

 proof

 let k2 be Nat;

 assume that

 A36: 1 <= k2 and

 A37: k2 <= ( len ( Col (A3,1)));



 A38: k2 in NAT by ORDINAL1:def 12;

 A39:

 now

 per cases by A36, XXREAL_0: 1;

 suppose k2 = 1;

 hence (A3 * (k2,1)) = (( Base_FinSeq (K,(k + 1),1)) . k2) by A10, A33, A37, Th24;

 end;

 suppose

 A40: 1 < k2;



 hence (A3 * (k2,1)) = ( 0. K) by A11, A33, A38, A37

 .= (( Base_FinSeq (K,(k + 1),1)) . k2) by A33, A37, A40, Th25;

 end;

 end;

 k2 in ( Seg ( len A3)) by A34, A33, A36, A37, FINSEQ_1: 1;

 then k2 in ( dom A3) by FINSEQ_1:def 3;

 hence thesis by A39, MATRIX_0:def 8;

 end;



 A41: ( len ( Line (B3,i))) = ( width B3) by MATRIX_0:def 7

 .= (k + 1) by MATRIX_0: 24;

 assume

 A42: 1 < i & i <= (k + 1);

 then

 A43: 1 <= (k + 1) by XXREAL_0: 2;



 A44: ( width B3) = (k + 1) by MATRIX_0: 24;

 then

 A45: 1 in ( Seg ( width B3)) by A43, FINSEQ_1: 1;

 [i, 1] in ( Indices (B3 * A3)) by A42, A43, MATRIX_0: 31;



 then ((B3 * A3) * (i,1)) = |(( Line (B3,i)), ( Col (A3,1)))| by A44, A34, MATRIX_3:def 4

 .= |(( Line (B3,i)), ( Base_FinSeq (K,(k + 1),1)))| by A33, A32, A35, FINSEQ_1: 14

 .= (( Line (B3,i)) . 1) by A43, A41, Th35

 .= (B3 * (i,1)) by A45, MATRIX_0:def 7;

 hence thesis by A30;

 end;



 A46: k in NAT by ORDINAL1:def 12;

 for i,j be Nat st 1 <= i & i <= k & 1 <= j & j <= k holds ((G * F) * (i,j)) = ( IFEQ (i,j,( 1. K),( 0. K)))

 proof

 let i,j be Nat;

 assume that

 A47: 1 <= i and

 A48: i <= k and

 A49: 1 <= j and

 A50: j <= k;



 A51: [i, j] in ( Indices (G * F)) by A47, A48, A49, A50, MATRIX_0: 31;



 A52: for k2 be Nat st k2 in ( dom <*( 0. K)*>) holds (( Col (A3,(j + 1))) . k2) = ( <*( 0. K)*> . k2)

 proof

 (j + 1) <= (k + 1) & 1 < (j + 1) by A49, A50, NAT_1: 13, XREAL_1: 7;

 then

 A53: (A3 * (1,(j + 1))) = ( 0. K) by A12;

 let k2 be Nat;

 assume k2 in ( dom <*( 0. K)*>);

 then k2 in ( Seg ( len <*( 0. K)*>)) by FINSEQ_1:def 3;

 then k2 in {1} by FINSEQ_1: 2, FINSEQ_1: 40;

 then

 A54: k2 = 1 by TARSKI:def 1;

 1 <= (k + 1) by NAT_1: 11;

 then k2 in ( Seg ( len A3)) by A29, A54, FINSEQ_1: 1;

 then k2 in ( dom A3) by FINSEQ_1:def 3;

 then (( Col (A3,(j + 1))) . k2) = ( 0. K) by A54, A53, MATRIX_0:def 8;

 hence thesis by A54, FINSEQ_1: 40;

 end;



 A55: ( len ( Col (F,j))) = ( len F) by MATRIX_0:def 8

 .= k by MATRIX_0: 24;



 A56: (i + 1) <= (k + 1) by A48, XREAL_1: 7;



 A57: for k2 be Nat st k2 in ( dom <*( 0. K)*>) holds (( Line (B3,(i + 1))) . k2) = ( <*( 0. K)*> . k2)

 proof

 let k2 be Nat;



 A58: 1 < (i + 1) by A47, NAT_1: 13;

 1 <= (1 + k) by NAT_1: 11;

 then

 A59: [(i + 1), 1] in ( Indices ( 1. (K,(k + 1)))) by A56, A58, MATRIX_0: 31;



 A60: (B3 * ((i + 1),1)) = (( 1. (K,(k + 1))) * ((i + 1),1)) by A31, A56, A58

 .= ( 0. K) by A58, A59, MATRIX_1:def 3;

 assume k2 in ( dom <*( 0. K)*>);

 then k2 in ( Seg ( len <*( 0. K)*>)) by FINSEQ_1:def 3;

 then k2 in {1} by FINSEQ_1: 2, FINSEQ_1: 40;

 then

 A61: k2 = 1 by TARSKI:def 1;

 1 <= (k + 1) by NAT_1: 11;

 then k2 in ( Seg ( width B3)) by A13, A61, FINSEQ_1: 1;

 then (( Line (B3,(i + 1))) . k2) = ( 0. K) by A61, A60, MATRIX_0:def 7;

 hence thesis by A61, FINSEQ_1: 40;

 end;



 A62: for k2 be Nat st k2 in ( dom ( Col (F,j))) holds (( Col (A3,(j + 1))) . (( len <*( 0. K)*>) + k2)) = (( Col (F,j)) . k2)

 proof

 reconsider j0 = (j + 1) as Element of NAT ;

 let k2 be Nat;



 A63: ( len ( Col (F,(j0 -' 1)))) = ( len F) by MATRIX_0:def 8;



 A64: (j0 -' 1) = j by NAT_D: 34;

 assume

 A65: k2 in ( dom ( Col (F,j)));

 then

 A66: k2 in ( Seg ( len ( Col (F,(j0 -' 1))))) by A64, FINSEQ_1:def 3;

 then

 A67: k2 <= k by A26, A63, FINSEQ_1: 1;

 then 1 <= (k2 + 1) & (k2 + 1) <= (k + 1) by NAT_1: 11, XREAL_1: 7;

 then

 A68: (k2 + 1) in ( dom A3) by A29, FINSEQ_3: 25;

 1 <= k2 by A66, FINSEQ_1: 1;

 then [k2, j] in ( Indices F) by A49, A50, A67, MATRIX_0: 31;

 then [k2, (j0 -' 1)] in ( Indices F) by NAT_D: 34;

 then

 A69: (A3 * ((k2 + 1),((j0 -' 1) + 1))) = (F * (k2,(j0 -' 1))) by A25;

 k2 in ( Seg k) by A26, A65, A63, A64, FINSEQ_1:def 3;

 then k2 in ( dom F) by A26, FINSEQ_1:def 3;

 then (A3 * ((k2 + 1),((j0 -' 1) + 1))) = (( Col (F,(j0 -' 1))) . k2) by A69, MATRIX_0:def 8;

 hence thesis by A23, A64, A68, MATRIX_0:def 8;

 end;



 A70: ( len ( Line (G,i))) = ( width G) by MATRIX_0:def 7

 .= k by MATRIX_0: 24;



 A71: (k + 1) = (( len <*( 0. K)*>) + k) by FINSEQ_1: 39;



 A72: for k2 be Nat st k2 in ( dom ( Line (G,i))) holds (( Line (B3,(i + 1))) . (( len <*( 0. K)*>) + k2)) = (( Line (G,i)) . k2)

 proof

 let k2 be Nat;



 A73: ( width B3) = (k + 1) & 1 <= (k2 + 1) by MATRIX_0: 24, NAT_1: 11;

 assume

 A74: k2 in ( dom ( Line (G,i)));

 then

 A75: k2 in ( Seg ( len ( Line (G,i)))) by FINSEQ_1:def 3;



 A76: ( len ( Line (G,i))) = ( width G) by MATRIX_0:def 7

 .= k by MATRIX_0: 24;

 then

 A77: k2 <= k by A75, FINSEQ_1: 1;

 1 <= k2 by A75, FINSEQ_1: 1;

 then [i, k2] in ( Indices G) by A47, A48, A77, MATRIX_0: 31;

 then

 A78: (B3 * ((i + 1),(k2 + 1))) = (G * (i,k2)) by A28;

 k2 in ( Seg k) by A74, A76, FINSEQ_1:def 3;

 then k2 in ( Seg ( width G)) by MATRIX_0: 24;

 then

 A79: (B3 * ((i + 1),(k2 + 1))) = (( Line (G,i)) . k2) by A78, MATRIX_0:def 7;

 (k2 + 1) <= (k + 1) by A77, XREAL_1: 7;

 then (k2 + 1) in ( Seg ( width B3)) by A73, FINSEQ_1: 1;

 then (( Line (B3,(i + 1))) . (k2 + 1)) = (( Line (G,i)) . k2) by A79, MATRIX_0:def 7;

 hence thesis by FINSEQ_1: 40;

 end;



 A80: ( width G) = k by MATRIX_0: 24;

 ( len ( Line (B3,(i + 1)))) = ( width B3) & ( len ( Line (G,i))) = ( width G) by MATRIX_0:def 7;

 then ( dom ( Line (B3,(i + 1)))) = ( Seg (( len <*( 0. K)*>) + ( len ( Line (G,i))))) by A13, A80, A71, FINSEQ_1:def 3;

 then

 A81: ( <*( 0. K)*> ^ ( Line (G,i))) = ( Line (B3,(i + 1))) by A57, A72, FINSEQ_1:def 7;



 A82: 1 <= (i + 1) & 1 <= (j + 1) by NAT_1: 11;



 A83: (j + 1) <= (k + 1) by A50, XREAL_1: 7;

 A84:

 now

 per cases ;

 suppose

 A85: i = j;

 [(i + 1), (j + 1)] in ( Indices ( 1. (K,(k + 1)))) by A82, A56, A83, MATRIX_0: 31;

 then (( 1. (K,(k + 1))) * ((i + 1),(j + 1))) = ( 1. K) by A85, MATRIX_1:def 3;

 hence (( 1. (K,(k + 1))) * ((i + 1),(j + 1))) = ( IFEQ (i,j,( 1. K),( 0. K))) by A85, FUNCOP_1:def 8;

 end;

 suppose

 A86: i <> j;

 [(i + 1), (j + 1)] in ( Indices ( 1. (K,(k + 1)))) by A82, A56, A83, MATRIX_0: 31;

 then (i + 1) <> (j + 1) implies (( 1. (K,(k + 1))) * ((i + 1),(j + 1))) = ( 0. K) by MATRIX_1:def 3;

 hence (( 1. (K,(k + 1))) * ((i + 1),(j + 1))) = ( IFEQ (i,j,( 1. K),( 0. K))) by A86, FUNCOP_1:def 8;

 end;

 end;

 ( len ( Col (A3,(j + 1)))) = ( len A3) & ( len ( Col (F,j))) = ( len F) by MATRIX_0:def 8;

 then ( dom ( Col (A3,(j + 1)))) = ( Seg (( len <*( 0. K)*>) + ( len ( Col (F,j))))) by A29, A26, A71, FINSEQ_1:def 3;

 then

 A87: ( <*( 0. K)*> ^ ( Col (F,j))) = ( Col (A3,(j + 1))) by A52, A62, FINSEQ_1:def 7;

 [(i + 1), (j + 1)] in ( Indices (B3 * A3)) by A82, A56, A83, MATRIX_0: 31;



 then ((B3 * A3) * ((i + 1),(j + 1))) = |(( Line (B3,(i + 1))), ( Col (A3,(j + 1))))| by A13, A29, MATRIX_3:def 4

 .= ( |( <*( 0. K)*>, <*( 0. K)*>)| + |(( Line (G,i)), ( Col (F,j)))|) by A23, A81, A87, A70, A55, Th12

 .= (( 0. K) + |(( Line (G,i)), ( Col (F,j)))|) by Th22

 .= |(( Line (G,i)), ( Col (F,j)))| by RLVECT_1: 4;

 hence thesis by A30, A26, A51, A80, A84, MATRIX_3:def 4;

 end;

 then (G * F) = ( 1. (K,k)) by Th29, A46;

 then

 consider G2 be Matrix of k, K such that

 A88: (F * G2) = ( 1. (K,k)) by A3;

 deffunc h( Nat, Nat) = ( IFEQ ($1,1,( IFEQ ($2,1,( 1. K),( 0. K))),( IFEQ ($2,1,( 0. K),(G2 * (($1 -' 1),($2 -' 1)))))));



 A89: ( len G2) = k by MATRIX_0: 24;

 consider B4 be Matrix of (k + 1), (k + 1), K such that

 A90: for i,j be Nat st [i, j] in ( Indices B4) holds (B4 * (i,j)) = h(i,j) from MATRIX_0:sch 1;



 A91: ( len B4) = (k + 1) by MATRIX_0: 24;



 A92: ( width B4) = (k + 1) by MATRIX_0: 24;



 A93: for j be Nat st 1 <= j & j <= ( len ( Col (B4,1))) holds (( Col (B4,1)) . j) = (( Base_FinSeq (K,(k + 1),1)) . j)

 proof

 let j be Nat;

 assume that

 A94: 1 <= j and

 A95: j <= ( len ( Col (B4,1)));



 A96: j <= (k + 1) by A91, A95, MATRIX_0:def 8;

 then 1 <= (k + 1) by A94, XXREAL_0: 2;

 then

 A97: [j, 1] in ( Indices B4) by A94, A96, MATRIX_0: 31;

 ( len ( Col (B4,1))) = ( len B4) by MATRIX_0:def 8;

 then j in ( Seg ( width B4)) by A91, A92, A94, A95, FINSEQ_1: 1;

 then

 A98: j in ( dom B4) by A91, A92, FINSEQ_1:def 3;

 per cases by A94, XXREAL_0: 1;

 suppose

 A99: 1 = j;

 (( Col (B4,1)) . j) = (B4 * (j,1)) by A98, MATRIX_0:def 8

 .= ( IFEQ (j,1,( IFEQ (1,1,( 1. K),( 0. K))),( IFEQ (1,1,( 0. K),(G2 * ((j -' 1),(1 -' 1))))))) by A90, A97

 .= ( IFEQ (1,1,( 1. K),( 0. K))) by A99, FUNCOP_1:def 8

 .= ( 1. K) by FUNCOP_1:def 8;

 hence thesis by A96, A99, Th24;

 end;

 suppose

 A100: 1 < j;

 (( Col (B4,1)) . j) = (B4 * (j,1)) by A98, MATRIX_0:def 8

 .= ( IFEQ (j,1,( IFEQ (1,1,( 1. K),( 0. K))),( IFEQ (1,1,( 0. K),(G2 * ((j -' 1),(1 -' 1))))))) by A90, A97

 .= ( IFEQ (1,1,( 0. K),(G2 * ((j -' 1),(1 -' 1))))) by A100, FUNCOP_1:def 8

 .= ( 0. K) by FUNCOP_1:def 8;

 hence thesis by A96, A100, Th25;

 end;

 end;



 A101: ( width (A3 * B4)) = (k + 1) by MATRIX_0: 24;



 A102: ( Indices (A3 * B4)) = [:( Seg (k + 1)), ( Seg (k + 1)):] by MATRIX_0: 24;

 ( len ( Line (A3,1))) = ( width A3) by MATRIX_0:def 7

 .= (k + 1) by MATRIX_0: 24;

 then

 A103: ( len ( Line (A3,1))) = ( len ( Base_FinSeq (K,(k + 1),1))) by Th23;

 then

 A104: ( Line (A3,1)) = ( Base_FinSeq (K,(k + 1),1)) by A15, FINSEQ_1: 14;



 A105: ( width F) = k by MATRIX_0: 24;



 A106: 1 <= (k + 1) by NAT_1: 11;

 ( len ( Col (B4,1))) = ( len B4) by MATRIX_0:def 8

 .= (k + 1) by MATRIX_0: 24;

 then

 A107: ( len ( Col (B4,1))) = ( len ( Base_FinSeq (K,(k + 1),1))) by Th23;

 then

 A108: ( Col (B4,1)) = ( Base_FinSeq (K,(k + 1),1)) by A93, FINSEQ_1: 14;

 for i,j be Nat st [i, j] in ( Indices (A3 * B4)) holds ((A3 * B4) * (i,j)) = (( 1. (K,(k + 1))) * (i,j))

 proof

 let i,j be Nat;

 reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def 12;



 A109: ( len ( Line (F,(i -' 1)))) = ( width F) by MATRIX_0:def 7

 .= k by MATRIX_0: 24;



 A110: ( len ( Col (G2,(j -' 1)))) = ( len G2) by MATRIX_0:def 8

 .= k by MATRIX_0: 24;



 A111: ( len ( Line (A3,i))) = ( width A3) by MATRIX_0:def 7

 .= (k + 1) by MATRIX_0: 24;



 A112: ( len ( Col (B4,j))) = ( len B4) by MATRIX_0:def 8

 .= (k + 1) by MATRIX_0: 24;

 assume

 A113: [i, j] in ( Indices (A3 * B4));

 then

 A114: [i, j] in [:( Seg (k + 1)), ( Seg (k + 1)):] by MATRIX_0: 24;

 then

 A115: [i, j] in ( Indices ( 1. (K,(k + 1)))) by MATRIX_0: 24;



 A116: i in ( Seg (k + 1)) by A102, A113, ZFMISC_1: 87;

 then

 A117: 1 <= i by FINSEQ_1: 1;



 A118: i <= (k + 1) by A116, FINSEQ_1: 1;



 A119: j in ( Seg (k + 1)) by A101, A113, ZFMISC_1: 87;

 then

 A120: 1 <= j by FINSEQ_1: 1;



 A121: ( len B4) = (k + 1) by MATRIX_0: 24;



 A122: ( width A3) = (k + 1) by MATRIX_0: 24;



 A123: j <= (k + 1) by A119, FINSEQ_1: 1;



 A124: [i, j] in ( Indices B4) by A102, A113, MATRIX_0: 24;

 now

 per cases by A117, XXREAL_0: 1;

 suppose

 A125: i = 1;

 now

 per cases by A120, XXREAL_0: 1;

 suppose

 A126: j = 1;

 ((A3 * B4) * (i,j)) = |(( Line (A3,i0)), ( Col (B4,j0)))| by A113, A121, A122, MATRIX_3:def 4

 .= ( 1. K) by A104, A108, A106, A125, A126, Th36;

 hence thesis by A115, A125, A126, MATRIX_1:def 3;

 end;

 suppose

 A127: j > 1;

 1 <= ( len B4) by A106, MATRIX_0: 24;

 then

 A128: 1 in ( dom B4) by FINSEQ_3: 25;

 ((A3 * B4) * (i,j)) = |(( Line (A3,i0)), ( Col (B4,j0)))| by A113, A121, A122, MATRIX_3:def 4

 .= |(( Base_FinSeq (K,(k + 1),1)), ( Col (B4,j0)))| by A103, A15, A125, FINSEQ_1: 14

 .= |(( Col (B4,j0)), ( Base_FinSeq (K,(k + 1),1)))| by FVSUM_1: 90

 .= (( Col (B4,j0)) . 1) by A106, A112, Th35

 .= (B4 * (1,j)) by A128, MATRIX_0:def 8

 .= ( IFEQ (i,1,( IFEQ (j,1,( 1. K),( 0. K))),( IFEQ (j,1,( 0. K),(G2 * ((i -' 1),(j -' 1))))))) by A90, A124, A125

 .= ( IFEQ (j,1,( 1. K),( 0. K))) by A125, FUNCOP_1:def 8

 .= ( 0. K) by A127, FUNCOP_1:def 8;

 hence thesis by A4, A114, A125, A127, MATRIX_1:def 3;

 end;

 end;

 hence thesis;

 end;

 suppose

 A129: 1 < i;

 then

 A130: (1 + 1) <= i by NAT_1: 13;

 now

 per cases by A120, XXREAL_0: 1;

 suppose

 A131: j = 1;



 A132: 1 in ( Seg ( width A3)) by A14, A106, FINSEQ_1: 1;



 A133: ( len ( Line (A3,i))) = ( width A3) by MATRIX_0:def 7

 .= (k + 1) by MATRIX_0: 24;

 ((A3 * B4) * (i,j)) = |(( Line (A3,i0)), ( Col (B4,j0)))| by A113, A121, A122, MATRIX_3:def 4

 .= |(( Line (A3,i)), ( Base_FinSeq (K,(k + 1),1)))| by A107, A93, A131, FINSEQ_1: 14

 .= (( Line (A3,i)) . 1) by A106, A133, Th35

 .= (((B * A2) * C) * (i0,1)) by A132, MATRIX_0:def 7

 .= ( 0. K) by A11, A118, A129;

 hence thesis by A115, A129, A131, MATRIX_1:def 3;

 end;

 suppose

 A134: j > 1;

 then (1 + 1) <= j by NAT_1: 13;

 then

 A135: 1 <= (j - 1) by XREAL_1: 19;



 A136: (i -' 1) = (i - 1) by A129, XREAL_1: 233;

 then

 A137: (i -' 1) <= k by A118, XREAL_1: 20;



 A138: 1 <= (i - 1) by A130, XREAL_1: 19;

 then

 A139: (i -' 1) in ( Seg k) by A136, A137, FINSEQ_1: 1;



 A140: ( len ( Line (F,(i -' 1)))) = ( width F) by MATRIX_0:def 7

 .= k by MATRIX_0: 24;



 A141: for k2 be Nat st k2 in ( dom ( Line (F,(i -' 1)))) holds (( Line (A3,((i -' 1) + 1))) . (( len <*( 0. K)*>) + k2)) = (( Line (F,(i -' 1))) . k2)

 proof

 let k2 be Nat;

 assume

 A142: k2 in ( dom ( Line (F,(i -' 1))));

 then

 A143: k2 in ( Seg ( len ( Line (F,(i -' 1))))) by FINSEQ_1:def 3;

 then

 A144: k2 <= k by A140, FINSEQ_1: 1;

 then 1 <= (k2 + 1) & (k2 + 1) <= (k + 1) by NAT_1: 11, XREAL_1: 7;

 then

 A145: (k2 + 1) in ( Seg ( width A3)) by A122, FINSEQ_1: 1;

 1 <= k2 by A143, FINSEQ_1: 1;

 then [(i -' 1), k2] in ( Indices F) by A136, A138, A137, A144, MATRIX_0: 31;

 then

 A146: (A3 * (((i -' 1) + 1),(k2 + 1))) = (F * ((i -' 1),k2)) by A25;

 k2 in ( Seg ( width F)) by A105, A140, A142, FINSEQ_1:def 3;

 then (A3 * (((i -' 1) + 1),(k2 + 1))) = (( Line (F,(i -' 1))) . k2) by A146, MATRIX_0:def 7;

 then (( Line (A3,((i -' 1) + 1))) . (k2 + 1)) = (( Line (F,(i -' 1))) . k2) by A145, MATRIX_0:def 7;

 hence thesis by FINSEQ_1: 40;

 end;



 A147: for k2 be Nat st k2 in ( dom <*( 0. K)*>) holds (( Line (A3,((i -' 1) + 1))) . k2) = ( <*( 0. K)*> . k2)

 proof

 let k2 be Nat;

 assume k2 in ( dom <*( 0. K)*>);

 then k2 in ( Seg ( len <*( 0. K)*>)) by FINSEQ_1:def 3;

 then k2 in {1} by FINSEQ_1: 2, FINSEQ_1: 40;

 then

 A148: k2 = 1 by TARSKI:def 1;



 A149: (A3 * (i0,1)) = ( 0. K) by A11, A118, A129;

 1 <= (k + 1) by NAT_1: 11;

 then k2 in ( Seg ( width A3)) by A122, A148, FINSEQ_1: 1;

 then (( Line (A3,i)) . k2) = ( 0. K) by A148, A149, MATRIX_0:def 7;

 hence thesis by A136, A148, FINSEQ_1: 40;

 end;

 ( dom ( Line (A3,((i -' 1) + 1)))) = ( Seg (k + 1)) by A111, A136, FINSEQ_1:def 3

 .= ( Seg (( len <*( 0. K)*>) + ( len ( Line (F,(i -' 1)))))) by A140, FINSEQ_1: 39;

 then

 A150: ( <*( 0. K)*> ^ ( Line (F,(i -' 1)))) = ( Line (A3,((i -' 1) + 1))) by A147, A141, FINSEQ_1:def 7;



 A151: ((j -' 1) + 1) = ((j - 1) + 1) by A134, XREAL_1: 233

 .= j;



 A152: (j -' 1) = (j - 1) by A134, XREAL_1: 233;

 then (j -' 1) <= k by A123, XREAL_1: 20;

 then (j -' 1) in ( Seg k) by A152, A135, FINSEQ_1: 1;

 then

 A153: [(i -' 1), (j -' 1)] in [:( Seg k), ( Seg k):] by A139, ZFMISC_1: 87;

 then

 A154: [(i -' 1), (j -' 1)] in ( Indices (F * G2)) by MATRIX_0: 24;



 A155: for k2 be Nat st k2 in ( dom <*( 0. K)*>) holds (( Col (B4,((j -' 1) + 1))) . k2) = ( <*( 0. K)*> . k2)

 proof

 1 <= (1 + k) by NAT_1: 11;

 then [1, j] in ( Indices B4) by A120, A123, MATRIX_0: 31;

 then (B4 * (1,j)) = ( IFEQ (1,1,( IFEQ (j,1,( 1. K),( 0. K))),( IFEQ (j,1,( 0. K),(G2 * ((1 -' 1),(j -' 1))))))) by A90;



 then

 A156: (B4 * (1,j)) = ( IFEQ (j,1,( 1. K),( 0. K))) by FUNCOP_1:def 8

 .= ( 0. K) by A134, FUNCOP_1:def 8;

 let k2 be Nat;

 assume k2 in ( dom <*( 0. K)*>);

 then k2 in ( Seg ( len <*( 0. K)*>)) by FINSEQ_1:def 3;

 then k2 in {1} by FINSEQ_1: 2, FINSEQ_1: 40;

 then

 A157: k2 = 1 by TARSKI:def 1;

 1 <= (k + 1) by NAT_1: 11;

 then k2 in ( Seg ( len B4)) by A121, A157, FINSEQ_1: 1;

 then k2 in ( dom B4) by FINSEQ_1:def 3;

 then (( Col (B4,j)) . k2) = ( 0. K) by A157, A156, MATRIX_0:def 8;

 hence thesis by A152, A157, FINSEQ_1: 40;

 end;



 A158: ( len ( Col (G2,(j -' 1)))) = ( len G2) by MATRIX_0:def 8

 .= k by MATRIX_0: 24;



 A159: for k2 be Nat st k2 in ( dom ( Col (G2,(j -' 1)))) holds (( Col (B4,((j -' 1) + 1))) . (( len <*( 0. K)*>) + k2)) = (( Col (G2,(j -' 1))) . k2)

 proof

 let k2 be Nat;

 assume

 A160: k2 in ( dom ( Col (G2,(j -' 1))));

 then 1 <= k2 by FINSEQ_3: 25;

 then

 A161: 1 < (k2 + 1) by NAT_1: 13;

 k2 in ( Seg k) by A158, A160, FINSEQ_1:def 3;

 then

 A162: k2 in ( dom G2) by A89, FINSEQ_1:def 3;

 k2 <= k by A158, A160, FINSEQ_3: 25;

 then

 A163: 1 <= (k2 + 1) & (k2 + 1) <= (k + 1) by NAT_1: 11, XREAL_1: 7;

 then [(k2 + 1), j] in ( Indices B4) by A120, A123, MATRIX_0: 31;

 then (B4 * ((k2 + 1),j)) = ( IFEQ ((k2 + 1),1,( IFEQ (j,1,( 1. K),( 0. K))),( IFEQ (j,1,( 0. K),(G2 * (((k2 + 1) -' 1),(j -' 1))))))) by A90;



 then (B4 * ((k2 + 1),j)) = ( IFEQ (j,1,( 0. K),(G2 * (((k2 + 1) -' 1),(j -' 1))))) by A161, FUNCOP_1:def 8

 .= (G2 * (((k2 + 1) -' 1),(j -' 1))) by A134, FUNCOP_1:def 8

 .= (G2 * (k2,(j -' 1))) by NAT_D: 34;

 then

 A164: (B4 * ((k2 + 1),((j -' 1) + 1))) = (( Col (G2,(j -' 1))) . k2) by A152, A162, MATRIX_0:def 8;

 (k2 + 1) in ( dom B4) by A121, A163, FINSEQ_3: 25;

 then (( Col (B4,((j -' 1) + 1))) . (k2 + 1)) = (( Col (G2,(j -' 1))) . k2) by A164, MATRIX_0:def 8;

 hence thesis by FINSEQ_1: 40;

 end;

 ( dom ( Col (B4,((j -' 1) + 1)))) = ( Seg ( len ( Col (B4,((j -' 1) + 1))))) by FINSEQ_1:def 3

 .= ( Seg (( len <*( 0. K)*>) + ( len ( Col (G2,(j -' 1)))))) by A112, A152, A158, FINSEQ_1: 39;

 then

 A165: ( <*( 0. K)*> ^ ( Col (G2,(j -' 1)))) = ( Col (B4,((j -' 1) + 1))) by A155, A159, FINSEQ_1:def 7;

 ((i -' 1) + 1) = ((i - 1) + 1) by A129, XREAL_1: 233

 .= i;



 then

 A166: ((A3 * B4) * (i,j)) = |(( Line (A3,((i -' 1) + 1))), ( Col (B4,((j -' 1) + 1))))| by A113, A121, A122, A151, MATRIX_3:def 4

 .= ( |( <*( 0. K)*>, <*( 0. K)*>)| + |(( Line (F,(i -' 1))), ( Col (G2,(j -' 1))))|) by A23, A109, A110, A150, A165, Th12

 .= (( 0. K) + |(( Line (F,(i -' 1))), ( Col (G2,(j -' 1))))|) by Th22

 .= (( 0. K) + ((F * G2) * ((i -' 1),(j -' 1)))) by A105, A89, A154, MATRIX_3:def 4

 .= (( 1. (K,k)) * ((i -' 1),(j -' 1))) by A88, RLVECT_1: 4;



 A167: [(i -' 1), (j -' 1)] in ( Indices ( 1. (K,k))) by A153, MATRIX_0: 24;

 now

 per cases ;

 suppose

 A168: i = j;

 then (( 1. (K,(k + 1))) * (i0,j0)) = ( 1. K) by A115, MATRIX_1:def 3;

 hence thesis by A167, A166, A168, MATRIX_1:def 3;

 end;

 suppose

 A169: i <> j;

 then (i - 1) <> (j - 1);

 then (i0 -' 1) <> (j0 -' 1) by A129, A152, XREAL_1: 233;

 then (( 1. (K,k)) * ((i0 -' 1),(j0 -' 1))) = ( 0. K) by A167, MATRIX_1:def 3;

 hence thesis by A115, A166, A169, MATRIX_1:def 3;

 end;

 end;

 hence thesis;

 end;

 end;

 hence thesis;

 end;

 end;

 hence thesis;

 end;

 then ( width ( Inv B)) = (k + 1) & (((B * A2) * C) * B4) = ( 1. (K,(k + 1))) by MATRIX_0: 24, MATRIX_0: 27;

 then (( Inv B) * (((B * A2) * C) * B4)) = ( Inv B) by MATRIXR2: 67;

 then ((( Inv B) * (((B * A2) * C) * B4)) * B) = ( 1. (K,(k + 1))) by A8, Th18;

 then ((( Inv B) * ((B * A2) * (C * B4))) * B) = ( 1. (K,(k + 1))) by Th17;

 then ((( Inv B) * (B * (A2 * (C * B4)))) * B) = ( 1. (K,(k + 1))) by Th17;

 then (((( Inv B) * B) * (A2 * (C * B4))) * B) = ( 1. (K,(k + 1))) by Th17;

 then ( len (A2 * (C * B4))) = (k + 1) & ((( 1. (K,(k + 1))) * (A2 * (C * B4))) * B) = ( 1. (K,(k + 1))) by A8, Th18, MATRIX_0: 24;

 then ((A2 * (C * B4)) * B) = ( 1. (K,(k + 1))) by MATRIXR2: 68;

 then (A2 * ((C * B4) * B)) = ( 1. (K,(k + 1))) by Th17;

 hence thesis;

 end;

 hence thesis;

 end;

 for D,B0 be Matrix of 0 , K st (B0 * D) = ( 1. (K, 0 )) holds ex B1 be Matrix of 0 , K st (D * B1) = ( 1. (K, 0 ))

 proof

 let D,B0 be Matrix of 0 , K;

 assume (B0 * D) = ( 1. (K, 0 ));

 (D * ( 0. (K, 0 ))) = ( 1. (K, 0 )) by Th15;

 hence thesis;

 end;

 then

 A170: P[ 0 ];

 for k be Nat holds P[k] from NAT_1:sch 2( A170, A2);

 hence thesis by A1;

 end;

 end;

 theorem :: MATRIX14:55



 Th55: for A be Matrix of n, K holds (ex B1 be Matrix of n, K st (B1 * A) = ( 1. (K,n))) iff ex B2 be Matrix of n, K st (A * B2) = ( 1. (K,n))

 proof

 let A be Matrix of n, K;

 per cases ;

 suppose

 A1: n > 0 ;

 thus (ex B be Matrix of n, K st (B * A) = ( 1. (K,n))) implies ex B2 be Matrix of n, K st (A * B2) = ( 1. (K,n)) by Th54;

 thus (ex B be Matrix of n, K st (A * B) = ( 1. (K,n))) implies ex B2 be Matrix of n, K st (B2 * A) = ( 1. (K,n))

 proof

 assume ex B be Matrix of n, K st (A * B) = ( 1. (K,n));

 then

 consider B be Matrix of n, K such that

 A2: (A * B) = ( 1. (K,n));



 A3: ( width A) = n & ( len B) = n by MATRIX_0: 24;

 ( width B) = n & ((A * B) @ ) = ( 1. (K,n)) by A2, MATRIX_0: 24, MATRIX_6: 10;

 then ((B @ ) * (A @ )) = ( 1. (K,n)) by A1, A3, MATRIX_3: 22;

 then

 consider B2 be Matrix of n, K such that

 A4: ((A @ ) * B2) = ( 1. (K,n)) by Th54;



 A5: ( width (A @ )) = n & ( len B2) = n by MATRIX_0: 24;

 ( width B2) = n & (((A @ ) * B2) @ ) = ( 1. (K,n)) by A4, MATRIX_0: 24, MATRIX_6: 10;

 then ((B2 @ ) * ((A @ ) @ )) = ( 1. (K,n)) by A1, A5, MATRIX_3: 22;

 then ((B2 @ ) * A) = ( 1. (K,n)) by MATRIXR2: 29;

 hence thesis;

 end;

 end;

 suppose

 A6: n = 0 ;

 then (A * A) = ( 1. (K, 0 )) by Th15;

 hence thesis by A6;

 end;

 end;

 theorem :: MATRIX14:56

 for A,B be Matrix of n, K st (A * B) = ( 1. (K,n)) holds A is invertible & B is invertible

 proof

 let A,B be Matrix of n, K;

 assume

 A1: (A * B) = ( 1. (K,n));

 then

 consider B2 be Matrix of n, K such that

 A2: (B2 * A) = ( 1. (K,n)) by Th55;

 B2 = (B2 * ( 1. (K,n))) by MATRIX_3: 19

 .= ((B2 * A) * B) by A1, Th17

 .= B by A2, MATRIX_3: 18;

 then A is_reverse_of B by A1, A2, MATRIX_6:def 2;

 hence A is invertible by MATRIX_6:def 3;

 consider B3 be Matrix of n, K such that

 A3: (B * B3) = ( 1. (K,n)) by A1, Th54;

 B3 = (( 1. (K,n)) * B3) by MATRIX_3: 18

 .= (A * (B * B3)) by A1, Th17

 .= A by A3, MATRIX_3: 19;

 then B is_reverse_of A by A1, A3, MATRIX_6:def 2;

 hence thesis by MATRIX_6:def 3;

 end;