:: MATRIX_5 semantic presentation

begin

theorem :: MATRIX_5:1
1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) = 1_ F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( complex ) Element of the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) ;

theorem :: MATRIX_5:2
0. F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( complex zero ) Element of the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ;

definition
let A be ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ;
func COMPLEX2Field A -> ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) equals :: MATRIX_5:def 1
A : ( ( ) ( ) L1()) ;
end;

definition
let A be ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) ;
func Field2COMPLEX A -> ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) equals :: MATRIX_5:def 2
A : ( ( ) ( ) L1()) ;
end;

theorem :: MATRIX_5:3
for A, B being ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) st COMPLEX2Field A : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) = COMPLEX2Field B : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) holds
A : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) = B : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ;

theorem :: MATRIX_5:4
for A, B being ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) st Field2COMPLEX A : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) = Field2COMPLEX B : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) holds
A : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) = B : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) ;

theorem :: MATRIX_5:5
for A being ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) holds A : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) = Field2COMPLEX (COMPLEX2Field A : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ;

theorem :: MATRIX_5:6
for A being ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) holds A : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) = COMPLEX2Field (Field2COMPLEX A : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) ;

definition
let A, B be ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ;
func A + B -> ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) equals :: MATRIX_5:def 3
 Field2COMPLEX ((COMPLEX2Field A : ( ( ) ( ) L1()) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) + (COMPLEX2Field B : ( ( ) ( ) VectSpStr over A : ( ( ) ( ) L1()) ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) FinSequence of K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ;
end;

definition
let A be ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ;
func - A -> ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) equals :: MATRIX_5:def 4
 Field2COMPLEX (- (COMPLEX2Field A : ( ( ) ( ) L1()) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) FinSequence of K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ;
end;

definition
let A, B be ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ;
func A - B -> ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) equals :: MATRIX_5:def 5
 Field2COMPLEX ((COMPLEX2Field A : ( ( ) ( ) L1()) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) - (COMPLEX2Field B : ( ( ) ( ) VectSpStr over A : ( ( ) ( ) L1()) ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) FinSequence of K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ;
func A * B -> ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) equals :: MATRIX_5:def 6
 Field2COMPLEX ((COMPLEX2Field A : ( ( ) ( ) L1()) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) * (COMPLEX2Field B : ( ( ) ( ) VectSpStr over A : ( ( ) ( ) L1()) ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) FinSequence of K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ;
end;

definition
let x be ( ( complex ) ( complex ) number ) ;
let A be ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ;
func x * A -> ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) means :: MATRIX_5:def 7
 for ea being ( ( ) ( complex ) Element of ( ( ) ( non zero V12() ) set ) ) st ea : ( ( ) ( complex ) Element of ( ( ) ( non zero V12() ) set ) ) = x : ( ( ) ( ) L1()) holds
it : ( ( Function-like V18(K20(A : ( ( ) ( ) VectSpStr over x : ( ( ) ( ) L1()) ) ,A : ( ( ) ( ) VectSpStr over x : ( ( ) ( ) L1()) ) ) : ( ( ) ( ) set ) ,A : ( ( ) ( ) VectSpStr over x : ( ( ) ( ) L1()) ) ) ) ( Relation-like K20(A : ( ( ) ( ) VectSpStr over x : ( ( ) ( ) L1()) ) ,A : ( ( ) ( ) VectSpStr over x : ( ( ) ( ) L1()) ) ) : ( ( ) ( ) set ) -defined A : ( ( ) ( ) VectSpStr over x : ( ( ) ( ) L1()) ) -valued Function-like V18(K20(A : ( ( ) ( ) VectSpStr over x : ( ( ) ( ) L1()) ) ,A : ( ( ) ( ) VectSpStr over x : ( ( ) ( ) L1()) ) ) : ( ( ) ( ) set ) ,A : ( ( ) ( ) VectSpStr over x : ( ( ) ( ) L1()) ) ) ) Element of K19(K20(K20(A : ( ( ) ( ) VectSpStr over x : ( ( ) ( ) L1()) ) ,A : ( ( ) ( ) VectSpStr over x : ( ( ) ( ) L1()) ) ) : ( ( ) ( ) set ) ,A : ( ( ) ( ) VectSpStr over x : ( ( ) ( ) L1()) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = Field2COMPLEX (ea : ( ( ) ( complex ) Element of ( ( ) ( non zero V12() ) set ) ) * (COMPLEX2Field A : ( ( ) ( ) VectSpStr over x : ( ( ) ( ) L1()) ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) FinSequence of K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ;
end;

theorem :: MATRIX_5:7
for A being ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) holds
( len A : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) = len (COMPLEX2Field A : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) & width A : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) = width (COMPLEX2Field A : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: MATRIX_5:8
for A being ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) holds
( len A : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) = len (Field2COMPLEX A : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) & width A : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) = width (Field2COMPLEX A : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: MATRIX_5:9
for K being ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field)
for M being ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) holds (1_ K : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) * M : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) FinSequence of K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) ) = M : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) ;

theorem :: MATRIX_5:10
for M being ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) holds 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) * M : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) = M : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ;

theorem :: MATRIX_5:11
for K being ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field)
for a, b being ( ( ) ( ) Element of ( ( ) ( non zero V12() ) set ) )
for M being ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) holds a : ( ( ) ( ) Element of ( ( ) ( non zero V12() ) set ) ) * (b : ( ( ) ( ) Element of ( ( ) ( non zero V12() ) set ) ) * M : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) FinSequence of K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) FinSequence of K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) ) = (a : ( ( ) ( ) Element of ( ( ) ( non zero V12() ) set ) ) * b : ( ( ) ( ) Element of ( ( ) ( non zero V12() ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) * M : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) FinSequence of K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) ) ;

theorem :: MATRIX_5:12
for K being ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field)
for a, b being ( ( ) ( ) Element of ( ( ) ( non zero V12() ) set ) )
for M being ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) holds (a : ( ( ) ( ) Element of ( ( ) ( non zero V12() ) set ) ) + b : ( ( ) ( ) Element of ( ( ) ( non zero V12() ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) * M : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) FinSequence of K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) ) = (a : ( ( ) ( ) Element of ( ( ) ( non zero V12() ) set ) ) * M : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) FinSequence of K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) ) + (b : ( ( ) ( ) Element of ( ( ) ( non zero V12() ) set ) ) * M : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) FinSequence of K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) FinSequence of K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) ) ;

theorem :: MATRIX_5:13
for M being ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) holds M : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) + M : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) = 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) * M : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ;

theorem :: MATRIX_5:14
for M being ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) holds (M : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) + M : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) + M : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) = 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) * M : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ;

definition
let n, m be ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Nat) ;
func 0_Cx (n,m) -> ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) equals :: MATRIX_5:def 8
 Field2COMPLEX (0. (F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) ,n : ( ( ) ( ) L1()) ,m : ( ( ) ( ) VectSpStr over n : ( ( ) ( ) L1()) ) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of n : ( ( ) ( ) L1()) ,m : ( ( ) ( ) VectSpStr over n : ( ( ) ( ) L1()) ) , the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ;
end;

theorem :: MATRIX_5:15
for n, m being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) holds COMPLEX2Field (0_Cx (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ,m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) = 0. (F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) ,n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ,m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ,b2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) , the U1 of F_Complex : ( ( strict ) ( V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) doubleLoopStr ) : ( ( ) ( non zero V12() ) set ) ) ;

theorem :: MATRIX_5:16
for M1, M2 being ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) st len M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) = len M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) & width M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) = width M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) & M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) = M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) + M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) holds
M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) = 0_Cx ((len M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ,(width M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ;

theorem :: MATRIX_5:17
for M1, M2 being ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) st len M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) = len M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) & width M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) = width M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) & M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) + M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) = 0_Cx ((len M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ,(width M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) holds
M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) = - M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ;

theorem :: MATRIX_5:18
for M1, M2 being ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) st len M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) = len M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) & width M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) = width M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) & M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) - M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) = M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) holds
M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) = 0_Cx ((len M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ,(width M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ;

theorem :: MATRIX_5:19
for M being ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) holds M : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) + (0_Cx ((len M : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ,(width M : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) = M : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ;

theorem :: MATRIX_5:20
for K being ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field)
for b being ( ( ) ( ) Element of ( ( ) ( non zero V12() ) set ) )
for M1, M2 being ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) st len M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) = len M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) & width M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) = width M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( non zero V12() ) set ) ) * (M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) + M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) FinSequence of K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) FinSequence of K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) ) = (b : ( ( ) ( ) Element of ( ( ) ( non zero V12() ) set ) ) * M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) FinSequence of K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) ) + (b : ( ( ) ( ) Element of ( ( ) ( non zero V12() ) set ) ) * M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) FinSequence of K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) FinSequence of K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) ) ;

theorem :: MATRIX_5:21
for M1, M2 being ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) )
for a being ( ( complex ) ( complex ) number ) st len M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) = len M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) & width M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) = width M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) holds
a : ( ( complex ) ( complex ) number ) * (M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) + M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) = (a : ( ( complex ) ( complex ) number ) * M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) + (a : ( ( complex ) ( complex ) number ) * M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ;

theorem :: MATRIX_5:22
for K being ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field)
for M1, M2 being ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) st width M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) = len M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) & len M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) & len M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(0. (K : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) ,(len M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ,(width M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of len b2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) , width b2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) , the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) * M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) FinSequence of K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) ) = 0. (K : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) ,(len M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ,(width M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of len b2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) , width b3 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) , the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) ;

theorem :: MATRIX_5:23
for M1, M2 being ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) st width M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) = len M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) & len M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) & len M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(0_Cx ((len M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ,(width M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) * M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) = 0_Cx ((len M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ,(width M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ;

theorem :: MATRIX_5:24
for K being ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field)
for M1 being ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) st len M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(0. K : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) ) : ( ( ) ( zero ) Element of the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) * M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) FinSequence of K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) ) = 0. (K : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) ,(len M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ,(width M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of len b2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) , width b2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) : ( ( ) ( ) M10( the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) , the U1 of b1 : ( ( V42() V46() right_complementable almost_left_invertible V117() V119() V122() V123() V124() well-unital V136() ) ( V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital ) Field) : ( ( ) ( non zero V12() ) set ) ) ;

theorem :: MATRIX_5:25
for M1 being ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) st len M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) holds
0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) * M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) = 0_Cx ((len M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ,(width M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) ;

definition
let s be ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ;
let k be ( ( ) ( ) set ) ;
:: original: .
redefine func s . k -> ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V33() ) set ) ) ;
end;

theorem :: MATRIX_5:26
for i, j being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) )
for M1, M2 being ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) st len M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) holds
ex s being ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non zero V33() ) set ) -valued Function-like FinSequence-like complex-valued ) FinSequence of COMPLEX : ( ( ) ( non zero V33() ) set ) ) st
( len s : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non zero V33() ) set ) -valued Function-like FinSequence-like complex-valued ) FinSequence of COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) = len M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) & s : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non zero V33() ) set ) -valued Function-like FinSequence-like complex-valued ) FinSequence of COMPLEX : ( ( ) ( non zero V33() ) set ) ) . 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V33() ) set ) ) = (M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) * (i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V33() ) set ) ) * (M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) * (1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ,j : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V33() ) set ) ) & ( for k being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) st 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) <= k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) & k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) < len M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) holds
s : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non zero V33() ) set ) -valued Function-like FinSequence-like complex-valued ) FinSequence of COMPLEX : ( ( ) ( non zero V33() ) set ) ) . (k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V33() ) set ) ) = (s : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non zero V33() ) set ) -valued Function-like FinSequence-like complex-valued ) FinSequence of COMPLEX : ( ( ) ( non zero V33() ) set ) ) . k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V33() ) set ) ) + ((M1 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) * (i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ,(k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V33() ) set ) ) * (M2 : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) -defined K176(COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) -valued Function-like FinSequence-like tabular ) Matrix of ( ( ) ( ) M10( COMPLEX : ( ( ) ( non zero V33() ) set ) )) ) * ((k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) ,j : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K19(REAL : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V33() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V33() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V33() ) set ) ) ) ) ;