:: MATRIX_5 semantic presentation begin theorem :: MATRIX_5:1 1 = 1_ F_Complex by COMPLEX1:def_4, COMPLFLD:8; theorem :: MATRIX_5:2 0. F_Complex = 0 by COMPLFLD:7; definition let A be Matrix of COMPLEX; func COMPLEX2Field A -> Matrix of F_Complex equals :: MATRIX_5:def 1 A; coherence A is Matrix of F_Complex by COMPLFLD:def_1; end; :: deftheorem defines COMPLEX2Field MATRIX_5:def_1_:_ for A being Matrix of COMPLEX holds COMPLEX2Field A = A; definition let A be Matrix of F_Complex; func Field2COMPLEX A -> Matrix of COMPLEX equals :: MATRIX_5:def 2 A; coherence A is Matrix of COMPLEX by COMPLFLD:def_1; end; :: deftheorem defines Field2COMPLEX MATRIX_5:def_2_:_ for A being Matrix of F_Complex holds Field2COMPLEX A = A; theorem :: MATRIX_5:3 for A, B being Matrix of COMPLEX st COMPLEX2Field A = COMPLEX2Field B holds A = B ; theorem :: MATRIX_5:4 for A, B being Matrix of F_Complex st Field2COMPLEX A = Field2COMPLEX B holds A = B ; theorem :: MATRIX_5:5 for A being Matrix of COMPLEX holds A = Field2COMPLEX (COMPLEX2Field A) ; theorem :: MATRIX_5:6 for A being Matrix of F_Complex holds A = COMPLEX2Field (Field2COMPLEX A) ; definition let A, B be Matrix of COMPLEX; funcA + B -> Matrix of COMPLEX equals :: MATRIX_5:def 3 Field2COMPLEX ((COMPLEX2Field A) + (COMPLEX2Field B)); coherence Field2COMPLEX ((COMPLEX2Field A) + (COMPLEX2Field B)) is Matrix of COMPLEX ; end; :: deftheorem defines + MATRIX_5:def_3_:_ for A, B being Matrix of COMPLEX holds A + B = Field2COMPLEX ((COMPLEX2Field A) + (COMPLEX2Field B)); definition let A be Matrix of COMPLEX; func - A -> Matrix of COMPLEX equals :: MATRIX_5:def 4 Field2COMPLEX (- (COMPLEX2Field A)); coherence Field2COMPLEX (- (COMPLEX2Field A)) is Matrix of COMPLEX ; end; :: deftheorem defines - MATRIX_5:def_4_:_ for A being Matrix of COMPLEX holds - A = Field2COMPLEX (- (COMPLEX2Field A)); definition let A, B be Matrix of COMPLEX; funcA - B -> Matrix of COMPLEX equals :: MATRIX_5:def 5 Field2COMPLEX ((COMPLEX2Field A) - (COMPLEX2Field B)); coherence Field2COMPLEX ((COMPLEX2Field A) - (COMPLEX2Field B)) is Matrix of COMPLEX ; funcA * B -> Matrix of COMPLEX equals :: MATRIX_5:def 6 Field2COMPLEX ((COMPLEX2Field A) * (COMPLEX2Field B)); coherence Field2COMPLEX ((COMPLEX2Field A) * (COMPLEX2Field B)) is Matrix of COMPLEX ; end; :: deftheorem defines - MATRIX_5:def_5_:_ for A, B being Matrix of COMPLEX holds A - B = Field2COMPLEX ((COMPLEX2Field A) - (COMPLEX2Field B)); :: deftheorem defines * MATRIX_5:def_6_:_ for A, B being Matrix of COMPLEX holds A * B = Field2COMPLEX ((COMPLEX2Field A) * (COMPLEX2Field B)); definition let x be complex number ; let A be Matrix of COMPLEX; funcx * A -> Matrix of COMPLEX means :Def7: :: MATRIX_5:def 7 for ea being Element of F_Complex st ea = x holds it = Field2COMPLEX (ea * (COMPLEX2Field A)); existence ex b1 being Matrix of COMPLEX st for ea being Element of F_Complex st ea = x holds b1 = Field2COMPLEX (ea * (COMPLEX2Field A)) proof x in COMPLEX by XCMPLX_0:def_2; then reconsider aa = x as Element of F_Complex by COMPLFLD:def_1; set C = Field2COMPLEX (aa * (COMPLEX2Field A)); for ea being Element of F_Complex st ea = x holds Field2COMPLEX (aa * (COMPLEX2Field A)) = Field2COMPLEX (ea * (COMPLEX2Field A)) ; hence ex b1 being Matrix of COMPLEX st for ea being Element of F_Complex st ea = x holds b1 = Field2COMPLEX (ea * (COMPLEX2Field A)) ; ::_thesis: verum end; uniqueness for b1, b2 being Matrix of COMPLEX st ( for ea being Element of F_Complex st ea = x holds b1 = Field2COMPLEX (ea * (COMPLEX2Field A)) ) & ( for ea being Element of F_Complex st ea = x holds b2 = Field2COMPLEX (ea * (COMPLEX2Field A)) ) holds b1 = b2 proof x in COMPLEX by XCMPLX_0:def_2; then reconsider aa = x as Element of F_Complex by COMPLFLD:def_1; let C1, C2 be Matrix of COMPLEX; ::_thesis: ( ( for ea being Element of F_Complex st ea = x holds C1 = Field2COMPLEX (ea * (COMPLEX2Field A)) ) & ( for ea being Element of F_Complex st ea = x holds C2 = Field2COMPLEX (ea * (COMPLEX2Field A)) ) implies C1 = C2 ) assume that A1: for ea being Element of F_Complex st ea = x holds C1 = Field2COMPLEX (ea * (COMPLEX2Field A)) and A2: for ea being Element of F_Complex st ea = x holds C2 = Field2COMPLEX (ea * (COMPLEX2Field A)) ; ::_thesis: C1 = C2 C2 = Field2COMPLEX (aa * (COMPLEX2Field A)) by A2; hence C1 = C2 by A1; ::_thesis: verum end; end; :: deftheorem Def7 defines * MATRIX_5:def_7_:_ for x being complex number for A, b3 being Matrix of COMPLEX holds ( b3 = x * A iff for ea being Element of F_Complex st ea = x holds b3 = Field2COMPLEX (ea * (COMPLEX2Field A)) ); theorem :: MATRIX_5:7 for A being Matrix of COMPLEX holds ( len A = len (COMPLEX2Field A) & width A = width (COMPLEX2Field A) ) ; theorem :: MATRIX_5:8 for A being Matrix of F_Complex holds ( len A = len (Field2COMPLEX A) & width A = width (Field2COMPLEX A) ) ; theorem Th9: :: MATRIX_5:9 for K being Field for M being Matrix of K holds (1_ K) * M = M proof let K be Field; ::_thesis: for M being Matrix of K holds (1_ K) * M = M let M be Matrix of K; ::_thesis: (1_ K) * M = M A1: for i, j being Nat st [i,j] in Indices M holds ((1_ K) * M) * (i,j) = M * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices M implies ((1_ K) * M) * (i,j) = M * (i,j) ) A2: (1_ K) * (M * (i,j)) = M * (i,j) by VECTSP_1:def_8; assume [i,j] in Indices M ; ::_thesis: ((1_ K) * M) * (i,j) = M * (i,j) hence ((1_ K) * M) * (i,j) = M * (i,j) by A2, MATRIX_3:def_5; ::_thesis: verum end; ( len ((1_ K) * M) = len M & width ((1_ K) * M) = width M ) by MATRIX_3:def_5; hence (1_ K) * M = M by A1, MATRIX_1:21; ::_thesis: verum end; theorem :: MATRIX_5:10 for M being Matrix of COMPLEX holds 1 * M = M proof set e = 1_ F_Complex; let M be Matrix of COMPLEX; ::_thesis: 1 * M = M 1 * M = Field2COMPLEX ((1_ F_Complex) * (COMPLEX2Field M)) by Def7, COMPLEX1:def_4, COMPLFLD:8; hence 1 * M = M by Th9; ::_thesis: verum end; theorem :: MATRIX_5:11 for K being Field for a, b being Element of K for M being Matrix of K holds a * (b * M) = (a * b) * M proof let K be Field; ::_thesis: for a, b being Element of K for M being Matrix of K holds a * (b * M) = (a * b) * M let a, b be Element of K; ::_thesis: for M being Matrix of K holds a * (b * M) = (a * b) * M let M be Matrix of K; ::_thesis: a * (b * M) = (a * b) * M A1: ( len ((a * b) * M) = len M & width ((a * b) * M) = width M ) by MATRIX_3:def_5; A2: len (a * (b * M)) = len (b * M) by MATRIX_3:def_5; A3: width (a * (b * M)) = width (b * M) by MATRIX_3:def_5; then A4: width (a * (b * M)) = width M by MATRIX_3:def_5; A5: ( len (b * M) = len M & width (b * M) = width M ) by MATRIX_3:def_5; A6: for i, j being Nat st [i,j] in Indices (a * (b * M)) holds (a * (b * M)) * (i,j) = ((a * b) * M) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * (b * M)) implies (a * (b * M)) * (i,j) = ((a * b) * M) * (i,j) ) assume A7: [i,j] in Indices (a * (b * M)) ; ::_thesis: (a * (b * M)) * (i,j) = ((a * b) * M) * (i,j) A8: Indices (b * M) = Indices M by A5, MATRIX_4:55; A9: Indices (a * (b * M)) = Indices (b * M) by A2, A3, MATRIX_4:55; then (a * (b * M)) * (i,j) = a * ((b * M) * (i,j)) by A7, MATRIX_3:def_5 .= a * (b * (M * (i,j))) by A7, A9, A8, MATRIX_3:def_5 .= (a * b) * (M * (i,j)) by GROUP_1:def_3 ; hence (a * (b * M)) * (i,j) = ((a * b) * M) * (i,j) by A7, A9, A8, MATRIX_3:def_5; ::_thesis: verum end; len (a * (b * M)) = len M by A2, MATRIX_3:def_5; hence a * (b * M) = (a * b) * M by A1, A4, A6, MATRIX_1:21; ::_thesis: verum end; theorem Th12: :: MATRIX_5:12 for K being Field for a, b being Element of K for M being Matrix of K holds (a + b) * M = (a * M) + (b * M) proof let K be Field; ::_thesis: for a, b being Element of K for M being Matrix of K holds (a + b) * M = (a * M) + (b * M) let a, b be Element of K; ::_thesis: for M being Matrix of K holds (a + b) * M = (a * M) + (b * M) let M be Matrix of K; ::_thesis: (a + b) * M = (a * M) + (b * M) A1: ( len (a * M) = len M & width (a * M) = width M ) by MATRIX_3:def_5; A2: ( len ((a + b) * M) = len M & width ((a + b) * M) = width M ) by MATRIX_3:def_5; A3: for i, j being Nat st [i,j] in Indices ((a + b) * M) holds ((a + b) * M) * (i,j) = ((a * M) + (b * M)) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices ((a + b) * M) implies ((a + b) * M) * (i,j) = ((a * M) + (b * M)) * (i,j) ) assume A4: [i,j] in Indices ((a + b) * M) ; ::_thesis: ((a + b) * M) * (i,j) = ((a * M) + (b * M)) * (i,j) A5: Indices ((a + b) * M) = Indices M by A2, MATRIX_4:55; Indices (a * M) = Indices M by A1, MATRIX_4:55; then ((a * M) + (b * M)) * (i,j) = ((a * M) * (i,j)) + ((b * M) * (i,j)) by A4, A5, MATRIX_3:def_3 .= (a * (M * (i,j))) + ((b * M) * (i,j)) by A4, A5, MATRIX_3:def_5 .= (a * (M * (i,j))) + (b * (M * (i,j))) by A4, A5, MATRIX_3:def_5 .= (a + b) * (M * (i,j)) by VECTSP_1:def_7 ; hence ((a + b) * M) * (i,j) = ((a * M) + (b * M)) * (i,j) by A4, A5, MATRIX_3:def_5; ::_thesis: verum end; ( len ((a * M) + (b * M)) = len (a * M) & width ((a * M) + (b * M)) = width (a * M) ) by MATRIX_3:def_3; hence (a + b) * M = (a * M) + (b * M) by A2, A1, A3, MATRIX_1:21; ::_thesis: verum end; theorem :: MATRIX_5:13 for M being Matrix of COMPLEX holds M + M = 2 * M proof reconsider e2 = (1_ F_Complex) + (1_ F_Complex) as Element of F_Complex ; let M be Matrix of COMPLEX; ::_thesis: M + M = 2 * M A1: (1_ F_Complex) * (COMPLEX2Field M) = COMPLEX2Field M by Th9; 2 * M = Field2COMPLEX (e2 * (COMPLEX2Field M)) by Def7, COMPLEX1:def_4, COMPLFLD:8 .= Field2COMPLEX ((COMPLEX2Field M) + (COMPLEX2Field M)) by A1, Th12 ; hence M + M = 2 * M ; ::_thesis: verum end; theorem :: MATRIX_5:14 for M being Matrix of COMPLEX holds (M + M) + M = 3 * M proof reconsider rr = 1 + 1 as Element of COMPLEX by XCMPLX_0:def_2; reconsider e3 = ((1_ F_Complex) + (1_ F_Complex)) + (1_ F_Complex) as Element of F_Complex ; let M be Matrix of COMPLEX; ::_thesis: (M + M) + M = 3 * M A1: ( len M = len (COMPLEX2Field M) & width M = width (COMPLEX2Field M) ) ; A2: (1_ F_Complex) + (1_ F_Complex) = the addF of F_Complex . ((1_ F_Complex),(1_ F_Complex)) by RLVECT_1:2 .= addcomplex . (1r,1r) by COMPLFLD:8, COMPLFLD:def_1 .= 1 + 1 by BINOP_2:def_3, COMPLEX1:def_4 ; ((1_ F_Complex) + (1_ F_Complex)) + (1_ F_Complex) = the addF of F_Complex . (((1_ F_Complex) + (1_ F_Complex)),(1_ F_Complex)) by RLVECT_1:2 .= addcomplex . ((1 + 1),1) by A2, COMPLFLD:def_1 .= rr + 1 by BINOP_2:def_3 .= 3 ; then 3 * M = Field2COMPLEX (e3 * (COMPLEX2Field M)) by Def7 .= Field2COMPLEX (((1_ F_Complex) * (COMPLEX2Field M)) + (((1_ F_Complex) + (1_ F_Complex)) * (COMPLEX2Field M))) by Th12 .= Field2COMPLEX ((COMPLEX2Field M) + (((1_ F_Complex) + (1_ F_Complex)) * (COMPLEX2Field M))) by Th9 .= Field2COMPLEX ((COMPLEX2Field M) + (((1_ F_Complex) * (COMPLEX2Field M)) + ((1_ F_Complex) * (COMPLEX2Field M)))) by Th12 .= Field2COMPLEX ((COMPLEX2Field M) + ((COMPLEX2Field M) + ((1_ F_Complex) * (COMPLEX2Field M)))) by Th9 .= Field2COMPLEX ((COMPLEX2Field M) + ((COMPLEX2Field M) + (COMPLEX2Field M))) by Th9 .= Field2COMPLEX (((COMPLEX2Field M) + (COMPLEX2Field M)) + (COMPLEX2Field M)) by A1, MATRIX_3:3 ; hence (M + M) + M = 3 * M ; ::_thesis: verum end; definition let n, m be Nat; func 0_Cx (n,m) -> Matrix of COMPLEX equals :: MATRIX_5:def 8 Field2COMPLEX (0. (F_Complex,n,m)); coherence Field2COMPLEX (0. (F_Complex,n,m)) is Matrix of COMPLEX ; end; :: deftheorem defines 0_Cx MATRIX_5:def_8_:_ for n, m being Nat holds 0_Cx (n,m) = Field2COMPLEX (0. (F_Complex,n,m)); theorem :: MATRIX_5:15 for n, m being Element of NAT holds COMPLEX2Field (0_Cx (n,m)) = 0. (F_Complex,n,m) ; theorem :: MATRIX_5:16 for M1, M2 being Matrix of COMPLEX st len M1 = len M2 & width M1 = width M2 & M1 = M1 + M2 holds M2 = 0_Cx ((len M1),(width M1)) proof let M1, M2 be Matrix of COMPLEX; ::_thesis: ( len M1 = len M2 & width M1 = width M2 & M1 = M1 + M2 implies M2 = 0_Cx ((len M1),(width M1)) ) assume that A1: ( len M1 = len M2 & width M1 = width M2 ) and A2: M1 = M1 + M2 ; ::_thesis: M2 = 0_Cx ((len M1),(width M1)) 0_Cx ((len M1),(width M1)) = (M1 + M2) + (- M1) by A2, MATRIX_4:2 .= Field2COMPLEX (((COMPLEX2Field M2) + (COMPLEX2Field M1)) - (COMPLEX2Field M1)) by A1, MATRIX_3:2 .= M2 by A1, MATRIX_4:21 ; hence M2 = 0_Cx ((len M1),(width M1)) ; ::_thesis: verum end; theorem :: MATRIX_5:17 for M1, M2 being Matrix of COMPLEX st len M1 = len M2 & width M1 = width M2 & M1 + M2 = 0_Cx ((len M1),(width M1)) holds M2 = - M1 proof let M1, M2 be Matrix of COMPLEX; ::_thesis: ( len M1 = len M2 & width M1 = width M2 & M1 + M2 = 0_Cx ((len M1),(width M1)) implies M2 = - M1 ) assume that A1: ( len M1 = len M2 & width M1 = width M2 ) and A2: M1 + M2 = 0_Cx ((len M1),(width M1)) ; ::_thesis: M2 = - M1 A3: ( len (- M2) = len M2 & width (- M2) = width M2 ) by MATRIX_3:def_2; COMPLEX2Field (0_Cx ((len M1),(width M1))) = (COMPLEX2Field M1) - (- (COMPLEX2Field M2)) by A2, MATRIX_4:1; then COMPLEX2Field M1 = - (COMPLEX2Field M2) by A1, A3, MATRIX_4:7; hence M2 = - M1 by MATRIX_4:1; ::_thesis: verum end; theorem :: MATRIX_5:18 for M1, M2 being Matrix of COMPLEX st len M1 = len M2 & width M1 = width M2 & M2 - M1 = M2 holds M1 = 0_Cx ((len M1),(width M1)) proof let M1, M2 be Matrix of COMPLEX; ::_thesis: ( len M1 = len M2 & width M1 = width M2 & M2 - M1 = M2 implies M1 = 0_Cx ((len M1),(width M1)) ) assume that A1: ( len M1 = len M2 & width M1 = width M2 ) and A2: M2 - M1 = M2 ; ::_thesis: M1 = 0_Cx ((len M1),(width M1)) (COMPLEX2Field M2) + (COMPLEX2Field M1) = COMPLEX2Field M2 by A1, A2, MATRIX_4:22; hence M1 = 0_Cx ((len M1),(width M1)) by A1, MATRIX_4:6; ::_thesis: verum end; theorem :: MATRIX_5:19 for M being Matrix of COMPLEX holds M + (0_Cx ((len M),(width M))) = M proof let M be Matrix of COMPLEX; ::_thesis: M + (0_Cx ((len M),(width M))) = M A1: ( len M = len (COMPLEX2Field M) & width M = width (COMPLEX2Field M) ) ; M + (0_Cx ((len M),(width M))) = M + (- (0_Cx ((len M),(width M)))) by MATRIX_4:9 .= Field2COMPLEX ((COMPLEX2Field M) - ((COMPLEX2Field M) - (COMPLEX2Field M))) by MATRIX_4:3 .= M by A1, MATRIX_4:11 ; hence M + (0_Cx ((len M),(width M))) = M ; ::_thesis: verum end; theorem Th20: :: MATRIX_5:20 for K being Field for b being Element of K for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds b * (M1 + M2) = (b * M1) + (b * M2) proof let K be Field; ::_thesis: for b being Element of K for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds b * (M1 + M2) = (b * M1) + (b * M2) let b be Element of K; ::_thesis: for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds b * (M1 + M2) = (b * M1) + (b * M2) let M1, M2 be Matrix of K; ::_thesis: ( len M1 = len M2 & width M1 = width M2 implies b * (M1 + M2) = (b * M1) + (b * M2) ) A1: ( len (b * (M1 + M2)) = len (M1 + M2) & width (b * (M1 + M2)) = width (M1 + M2) ) by MATRIX_3:def_5; A2: ( len (M1 + M2) = len M1 & width (M1 + M2) = width M1 ) by MATRIX_3:def_3; A3: ( len (b * M1) = len M1 & width (b * M1) = width M1 ) by MATRIX_3:def_5; assume A4: ( len M1 = len M2 & width M1 = width M2 ) ; ::_thesis: b * (M1 + M2) = (b * M1) + (b * M2) A5: for i, j being Nat st [i,j] in Indices (b * (M1 + M2)) holds (b * (M1 + M2)) * (i,j) = ((b * M1) + (b * M2)) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (b * (M1 + M2)) implies (b * (M1 + M2)) * (i,j) = ((b * M1) + (b * M2)) * (i,j) ) assume A6: [i,j] in Indices (b * (M1 + M2)) ; ::_thesis: (b * (M1 + M2)) * (i,j) = ((b * M1) + (b * M2)) * (i,j) A7: Indices M2 = Indices M1 by A4, MATRIX_4:55; A8: Indices (b * (M1 + M2)) = Indices (M1 + M2) by A1, MATRIX_4:55; A9: Indices (M1 + M2) = Indices M1 by A2, MATRIX_4:55; Indices (b * M1) = Indices M1 by A3, MATRIX_4:55; then ((b * M1) + (b * M2)) * (i,j) = ((b * M1) * (i,j)) + ((b * M2) * (i,j)) by A6, A8, A9, MATRIX_3:def_3 .= (b * (M1 * (i,j))) + ((b * M2) * (i,j)) by A6, A8, A9, MATRIX_3:def_5 .= (b * (M1 * (i,j))) + (b * (M2 * (i,j))) by A6, A8, A9, A7, MATRIX_3:def_5 .= b * ((M1 * (i,j)) + (M2 * (i,j))) by VECTSP_1:def_7 ; then ((b * M1) + (b * M2)) * (i,j) = b * ((M1 + M2) * (i,j)) by A6, A8, A9, MATRIX_3:def_3 .= (b * (M1 + M2)) * (i,j) by A6, A8, MATRIX_3:def_5 ; hence (b * (M1 + M2)) * (i,j) = ((b * M1) + (b * M2)) * (i,j) ; ::_thesis: verum end; ( len ((b * M1) + (b * M2)) = len (b * M1) & width ((b * M1) + (b * M2)) = width (b * M1) ) by MATRIX_3:def_3; hence b * (M1 + M2) = (b * M1) + (b * M2) by A1, A2, A3, A5, MATRIX_1:21; ::_thesis: verum end; theorem :: MATRIX_5:21 for M1, M2 being Matrix of COMPLEX for a being complex number st len M1 = len M2 & width M1 = width M2 holds a * (M1 + M2) = (a * M1) + (a * M2) proof let M1, M2 be Matrix of COMPLEX; ::_thesis: for a being complex number st len M1 = len M2 & width M1 = width M2 holds a * (M1 + M2) = (a * M1) + (a * M2) let a be complex number ; ::_thesis: ( len M1 = len M2 & width M1 = width M2 implies a * (M1 + M2) = (a * M1) + (a * M2) ) assume A1: ( len M1 = len M2 & width M1 = width M2 ) ; ::_thesis: a * (M1 + M2) = (a * M1) + (a * M2) a in COMPLEX by XCMPLX_0:def_2; then reconsider ea = a as Element of F_Complex by COMPLFLD:def_1; A2: (a * M1) + (a * M2) = Field2COMPLEX ((COMPLEX2Field (Field2COMPLEX (ea * (COMPLEX2Field M1)))) + (COMPLEX2Field (a * M2))) by Def7 .= Field2COMPLEX ((ea * (COMPLEX2Field M1)) + (COMPLEX2Field (Field2COMPLEX (ea * (COMPLEX2Field M2))))) by Def7 .= Field2COMPLEX ((ea * (COMPLEX2Field M1)) + (ea * (COMPLEX2Field M2))) ; a * (M1 + M2) = Field2COMPLEX (ea * (COMPLEX2Field (M1 + M2))) by Def7 .= Field2COMPLEX ((ea * (COMPLEX2Field M1)) + (ea * (COMPLEX2Field M2))) by A1, Th20 ; hence a * (M1 + M2) = (a * M1) + (a * M2) by A2; ::_thesis: verum end; theorem Th22: :: MATRIX_5:22 for K being Field for M1, M2 being Matrix of K st width M1 = len M2 & len M1 > 0 & len M2 > 0 holds (0. (K,(len M1),(width M1))) * M2 = 0. (K,(len M1),(width M2)) proof let K be Field; ::_thesis: for M1, M2 being Matrix of K st width M1 = len M2 & len M1 > 0 & len M2 > 0 holds (0. (K,(len M1),(width M1))) * M2 = 0. (K,(len M1),(width M2)) let M1, M2 be Matrix of K; ::_thesis: ( width M1 = len M2 & len M1 > 0 & len M2 > 0 implies (0. (K,(len M1),(width M1))) * M2 = 0. (K,(len M1),(width M2)) ) assume that A1: width M1 = len M2 and A2: len M1 > 0 and A3: len M2 > 0 ; ::_thesis: (0. (K,(len M1),(width M1))) * M2 = 0. (K,(len M1),(width M2)) A4: len (0. (K,(len M1),(width M1))) = len M1 by MATRIX_1:def_2; then A5: width (0. (K,(len M1),(width M1))) = width M1 by A2, MATRIX_1:20; then A6: len ((0. (K,(len M1),(width M1))) * M2) = len (0. (K,(len M1),(width M1))) by A1, MATRIX_3:def_4; A7: width ((0. (K,(len M1),(width M1))) * M2) = width M2 by A1, A5, MATRIX_3:def_4; set B = (0. (K,(len M1),(width M1))) * M2; A8: width (- ((0. (K,(len M1),(width M1))) * M2)) = width ((0. (K,(len M1),(width M1))) * M2) by MATRIX_3:def_2; (0. (K,(len M1),(width M1))) * M2 = ((0. (K,(len M1),(width M1))) + (0. (K,(len M1),(width M1)))) * M2 by MATRIX_3:4 .= ((0. (K,(len M1),(width M1))) * M2) + ((0. (K,(len M1),(width M1))) * M2) by A1, A2, A3, A4, A5, MATRIX_4:63 ; then ( len (- ((0. (K,(len M1),(width M1))) * M2)) = len ((0. (K,(len M1),(width M1))) * M2) & 0. (K,(len M1),(width M2)) = (((0. (K,(len M1),(width M1))) * M2) + ((0. (K,(len M1),(width M1))) * M2)) + (- ((0. (K,(len M1),(width M1))) * M2)) ) by A4, A6, A7, MATRIX_3:def_2, MATRIX_4:2; then 0. (K,(len M1),(width M2)) = ((0. (K,(len M1),(width M1))) * M2) + (((0. (K,(len M1),(width M1))) * M2) - ((0. (K,(len M1),(width M1))) * M2)) by A8, MATRIX_3:3 .= (0. (K,(len M1),(width M1))) * M2 by A6, A8, MATRIX_4:20 ; hence (0. (K,(len M1),(width M1))) * M2 = 0. (K,(len M1),(width M2)) ; ::_thesis: verum end; theorem :: MATRIX_5:23 for M1, M2 being Matrix of COMPLEX st width M1 = len M2 & len M1 > 0 & len M2 > 0 holds (0_Cx ((len M1),(width M1))) * M2 = 0_Cx ((len M1),(width M2)) proof let M1, M2 be Matrix of COMPLEX; ::_thesis: ( width M1 = len M2 & len M1 > 0 & len M2 > 0 implies (0_Cx ((len M1),(width M1))) * M2 = 0_Cx ((len M1),(width M2)) ) A1: len M1 = len (COMPLEX2Field M1) ; assume ( width M1 = len M2 & len M1 > 0 & len M2 > 0 ) ; ::_thesis: (0_Cx ((len M1),(width M1))) * M2 = 0_Cx ((len M1),(width M2)) hence (0_Cx ((len M1),(width M1))) * M2 = 0_Cx ((len M1),(width M2)) by A1, Th22; ::_thesis: verum end; theorem Th24: :: MATRIX_5:24 for K being Field for M1 being Matrix of K st len M1 > 0 holds (0. K) * M1 = 0. (K,(len M1),(width M1)) proof let K be Field; ::_thesis: for M1 being Matrix of K st len M1 > 0 holds (0. K) * M1 = 0. (K,(len M1),(width M1)) let M1 be Matrix of K; ::_thesis: ( len M1 > 0 implies (0. K) * M1 = 0. (K,(len M1),(width M1)) ) A1: len (0. (K,(len M1),(width M1))) = len M1 by MATRIX_1:def_2; assume len M1 > 0 ; ::_thesis: (0. K) * M1 = 0. (K,(len M1),(width M1)) then A2: width (0. (K,(len M1),(width M1))) = width M1 by A1, MATRIX_1:20; A3: for i, j being Nat st [i,j] in Indices (0. (K,(len M1),(width M1))) holds ((0. K) * M1) * (i,j) = (0. (K,(len M1),(width M1))) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (0. (K,(len M1),(width M1))) implies ((0. K) * M1) * (i,j) = (0. (K,(len M1),(width M1))) * (i,j) ) assume A4: [i,j] in Indices (0. (K,(len M1),(width M1))) ; ::_thesis: ((0. K) * M1) * (i,j) = (0. (K,(len M1),(width M1))) * (i,j) Indices (0. (K,(len M1),(width M1))) = Indices M1 by A1, A2, MATRIX_4:55; then A5: ((0. K) * M1) * (i,j) = (0. K) * (M1 * (i,j)) by A4, MATRIX_3:def_5; (0. (K,(len M1),(width M1))) * (i,j) = 0. K by A4, MATRIX_3:1; hence ((0. K) * M1) * (i,j) = (0. (K,(len M1),(width M1))) * (i,j) by A5, VECTSP_1:6; ::_thesis: verum end; ( len ((0. K) * M1) = len M1 & width ((0. K) * M1) = width M1 ) by MATRIX_3:def_5; hence (0. K) * M1 = 0. (K,(len M1),(width M1)) by A1, A2, A3, MATRIX_1:21; ::_thesis: verum end; theorem :: MATRIX_5:25 for M1 being Matrix of COMPLEX st len M1 > 0 holds 0 * M1 = 0_Cx ((len M1),(width M1)) proof reconsider ea = 0 as Element of F_Complex by COMPLFLD:def_1; let M1 be Matrix of COMPLEX; ::_thesis: ( len M1 > 0 implies 0 * M1 = 0_Cx ((len M1),(width M1)) ) assume A1: len M1 > 0 ; ::_thesis: 0 * M1 = 0_Cx ((len M1),(width M1)) 0 * M1 = Field2COMPLEX (ea * (COMPLEX2Field M1)) by Def7 .= 0_Cx ((len M1),(width M1)) by A1, Th24, COMPLFLD:7 ; hence 0 * M1 = 0_Cx ((len M1),(width M1)) ; ::_thesis: verum end; definition let s be complex-valued Function; let k be set ; :: original: . redefine funcs . k -> Element of COMPLEX ; coherence s . k is Element of COMPLEX proof percases ( k in dom s or not k in dom s ) ; supposeA1: k in dom s ; ::_thesis: s . k is Element of COMPLEX A2: rng s c= COMPLEX by VALUED_0:def_1; s . k in rng s by A1, FUNCT_1:def_3; hence s . k is Element of COMPLEX by A2; ::_thesis: verum end; suppose not k in dom s ; ::_thesis: s . k is Element of COMPLEX then s . k = 0c by FUNCT_1:def_2; hence s . k is Element of COMPLEX ; ::_thesis: verum end; end; end; end; theorem :: MATRIX_5:26 for i, j being Element of NAT for M1, M2 being Matrix of COMPLEX st len M2 > 0 holds ex s being FinSequence of COMPLEX st ( len s = len M2 & s . 1 = (M1 * (i,1)) * (M2 * (1,j)) & ( for k being Element of NAT st 1 <= k & k < len M2 holds s . (k + 1) = (s . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) ) proof let i, j be Element of NAT ; ::_thesis: for M1, M2 being Matrix of COMPLEX st len M2 > 0 holds ex s being FinSequence of COMPLEX st ( len s = len M2 & s . 1 = (M1 * (i,1)) * (M2 * (1,j)) & ( for k being Element of NAT st 1 <= k & k < len M2 holds s . (k + 1) = (s . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) ) let M1, M2 be Matrix of COMPLEX; ::_thesis: ( len M2 > 0 implies ex s being FinSequence of COMPLEX st ( len s = len M2 & s . 1 = (M1 * (i,1)) * (M2 * (1,j)) & ( for k being Element of NAT st 1 <= k & k < len M2 holds s . (k + 1) = (s . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) ) ) defpred S1[ Element of NAT ] means ex q being FinSequence of COMPLEX st ( 1 <= \$1 + 1 & \$1 + 1 <= len M2 implies ( len q = \$1 + 1 & q . 1 = (M1 * (i,1)) * (M2 * (1,j)) & ( for k being Element of NAT st 1 <= k & k < \$1 + 1 holds q . (k + 1) = (q . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) ) ); set q0 = <*((M1 * (i,1)) * (M2 * (1,j)))*>; A1: for k being Element of NAT st 1 <= k & k < 1 holds <*((M1 * (i,1)) * (M2 * (1,j)))*> . (k + 1) = (<*((M1 * (i,1)) * (M2 * (1,j)))*> . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ; A2: for i2 being Element of NAT st S1[i2] holds S1[i2 + 1] proof let i2 be Element of NAT ; ::_thesis: ( S1[i2] implies S1[i2 + 1] ) set k0 = i2; assume S1[i2] ; ::_thesis: S1[i2 + 1] then consider q2 being FinSequence of COMPLEX such that A3: ( 1 <= i2 + 1 & i2 + 1 <= len M2 implies ( len q2 = i2 + 1 & q2 . 1 = (M1 * (i,1)) * (M2 * (1,j)) & ( for k2 being Element of NAT st 1 <= k2 & k2 < i2 + 1 holds q2 . (k2 + 1) = (q2 . k2) + ((M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j))) ) ) ) ; set q3 = q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>; ( 1 <= (i2 + 1) + 1 & (i2 + 1) + 1 <= len M2 implies ( len (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) = (i2 + 1) + 1 & (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . 1 = (M1 * (i,1)) * (M2 * (1,j)) & ( for k being Element of NAT st 1 <= k & k < (i2 + 1) + 1 holds (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . (k + 1) = ((q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) ) ) proof assume that 1 <= (i2 + 1) + 1 and A4: (i2 + 1) + 1 <= len M2 ; ::_thesis: ( len (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) = (i2 + 1) + 1 & (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . 1 = (M1 * (i,1)) * (M2 * (1,j)) & ( for k being Element of NAT st 1 <= k & k < (i2 + 1) + 1 holds (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . (k + 1) = ((q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) ) percases 1 <= i2 + 1 by NAT_1:12; supposeA5: 1 <= i2 + 1 ; ::_thesis: ( len (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) = (i2 + 1) + 1 & (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . 1 = (M1 * (i,1)) * (M2 * (1,j)) & ( for k being Element of NAT st 1 <= k & k < (i2 + 1) + 1 holds (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . (k + 1) = ((q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) ) A6: len (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) = (len q2) + (len <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) by FINSEQ_1:22 .= (i2 + 1) + 1 by A3, A4, A5, FINSEQ_1:39, NAT_1:13 ; A7: for k2 being Element of NAT st 1 <= k2 & k2 < (i2 + 1) + 1 holds (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . (k2 + 1) = ((q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . k2) + ((M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j))) proof let k2 be Element of NAT ; ::_thesis: ( 1 <= k2 & k2 < (i2 + 1) + 1 implies (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . (k2 + 1) = ((q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . k2) + ((M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j))) ) assume that A8: 1 <= k2 and A9: k2 < (i2 + 1) + 1 ; ::_thesis: (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . (k2 + 1) = ((q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . k2) + ((M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j))) A10: k2 <= i2 + 1 by A9, NAT_1:13; percases ( k2 < i2 + 1 or k2 = i2 + 1 ) by A10, XXREAL_0:1; supposeA11: k2 < i2 + 1 ; ::_thesis: (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . (k2 + 1) = ((q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . k2) + ((M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j))) then k2 < len (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) by A6, NAT_1:13; then k2 < (len q2) + (len <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) by FINSEQ_1:22; then k2 < (len q2) + 1 by FINSEQ_1:39; then k2 <= len q2 by NAT_1:13; then k2 in dom q2 by A8, FINSEQ_3:25; then A12: (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . k2 = q2 . k2 by FINSEQ_1:def_7; k2 + 1 < (i2 + 1) + 1 by A11, XREAL_1:6; then k2 + 1 < (len q2) + (len <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) by A6, FINSEQ_1:22; then k2 + 1 < (len q2) + 1 by FINSEQ_1:39; then A13: k2 + 1 <= len q2 by NAT_1:13; 1 <= k2 + 1 by A8, NAT_1:13; then k2 + 1 in dom q2 by A13, FINSEQ_3:25; then (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . (k2 + 1) = q2 . (k2 + 1) by FINSEQ_1:def_7; hence (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . (k2 + 1) = ((q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . k2) + ((M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j))) by A3, A4, A5, A8, A11, A12, NAT_1:13; ::_thesis: verum end; supposeA14: k2 = i2 + 1 ; ::_thesis: (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . (k2 + 1) = ((q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . k2) + ((M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j))) then k2 < (i2 + 1) + 1 by NAT_1:13; then k2 < (len q2) + (len <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) by A6, FINSEQ_1:22; then k2 < (len q2) + 1 by FINSEQ_1:39; then k2 <= len q2 by NAT_1:13; then k2 in dom q2 by A8, FINSEQ_3:25; then A15: (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . k2 = q2 . k2 by FINSEQ_1:def_7; 1 in Seg 1 by FINSEQ_1:3; then ( <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*> . 1 = (q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))) & 1 in dom <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*> ) by FINSEQ_1:def_8; hence (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . (k2 + 1) = ((q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . k2) + ((M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j))) by A3, A4, A5, A14, A15, FINSEQ_1:def_7, NAT_1:13; ::_thesis: verum end; end; end; 1 < len (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) by A5, A6, NAT_1:13; then 1 < (len q2) + (len <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) by FINSEQ_1:22; then 1 < (len q2) + 1 by FINSEQ_1:39; then 1 <= len q2 by NAT_1:13; then 1 in dom q2 by FINSEQ_3:25; hence ( len (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) = (i2 + 1) + 1 & (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . 1 = (M1 * (i,1)) * (M2 * (1,j)) & ( for k being Element of NAT st 1 <= k & k < (i2 + 1) + 1 holds (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . (k + 1) = ((q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) ) by A3, A4, A5, A6, A7, FINSEQ_1:def_7, NAT_1:13; ::_thesis: verum end; end; end; hence S1[i2 + 1] ; ::_thesis: verum end; ( len <*((M1 * (i,1)) * (M2 * (1,j)))*> = 1 & <*((M1 * (i,1)) * (M2 * (1,j)))*> . 1 = (M1 * (i,1)) * (M2 * (1,j)) ) by FINSEQ_1:39, FINSEQ_1:def_8; then A16: S1[ 0 ] by A1; A17: for j being Element of NAT holds S1[j] from NAT_1:sch_1(A16, A2); assume A18: len M2 > 0 ; ::_thesis: ex s being FinSequence of COMPLEX st ( len s = len M2 & s . 1 = (M1 * (i,1)) * (M2 * (1,j)) & ( for k being Element of NAT st 1 <= k & k < len M2 holds s . (k + 1) = (s . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) ) then 0 + 1 <= len M2 by NAT_1:8; then (0 + 1) - 1 <= (len M2) - 1 by XREAL_1:9; then A19: (len M2) -' 1 = (len M2) - 1 by XREAL_0:def_2; then 0 + 1 <= ((len M2) -' 1) + 1 by A18, NAT_1:8; hence ex s being FinSequence of COMPLEX st ( len s = len M2 & s . 1 = (M1 * (i,1)) * (M2 * (1,j)) & ( for k being Element of NAT st 1 <= k & k < len M2 holds s . (k + 1) = (s . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) ) by A19, A17; ::_thesis: verum end;