:: MATRIX_1 semantic presentation

definition
let c1 be FinSequence;
attr a1 is tabular means :Def1: :: MATRIX_1:def 1
ex b1 being Nat st
for b2 being set st b2 in rng a1 holds
ex b3 being FinSequence st
( b3 = b2 & len b3 = b1 );
end;

:: deftheorem Def1 defines tabular MATRIX_1:def 1 :
for b1 being FinSequence holds
( b1 is tabular iff ex b2 being Nat st
for b3 being set st b3 in rng b1 holds
ex b4 being FinSequence st
( b4 = b3 & len b4 = b2 ) );

registration
cluster tabular set ;
existence
ex b1 being FinSequence st b1 is tabular
proof end;
end;

theorem Th1: :: MATRIX_1:1
for b1 being non empty set
for b2 being Element of b1 holds <*<*b2*>*> is tabular
proof end;

theorem Th2: :: MATRIX_1:2
for b1 being set
for b2, b3 being Nat holds b2 |-> (b3 |-> b1) is tabular
proof end;

theorem Th3: :: MATRIX_1:3
for b1 being FinSequence holds <*b1*> is tabular
proof end;

theorem Th4: :: MATRIX_1:4
for b1 being Nat
for b2, b3 being FinSequence st len b2 = b1 & len b3 = b1 holds
<*b2,b3*> is tabular
proof end;

theorem Th5: :: MATRIX_1:5
{} is tabular
proof end;

theorem Th6: :: MATRIX_1:6
<*{} ,{} *> is tabular
proof end;

theorem Th7: :: MATRIX_1:7
for b1 being non empty set
for b2, b3 being Element of b1 holds <*<*b2*>,<*b3*>*> is tabular
proof end;

theorem Th8: :: MATRIX_1:8
for b1 being non empty set
for b2, b3, b4, b5 being Element of b1 holds <*<*b2,b3*>,<*b4,b5*>*> is tabular
proof end;

registration
let c1 be set ;
cluster tabular FinSequence of a1 * ;
existence
ex b1 being FinSequence of c1 * st b1 is tabular
proof end;
end;

definition
let c1 be set ;
mode Matrix of a1 is tabular FinSequence of a1 * ;
end;

registration
let c1 be non empty set ;
cluster non empty-yielding FinSequence of a1 * ;
existence
not for b1 being Matrix of c1 holds b1 is empty-yielding
proof end;
end;

theorem Th9: :: MATRIX_1:9
for b1 being non empty set
for b2 being FinSequence holds
( b2 is Matrix of b1 iff ex b3 being Nat st
for b4 being set st b4 in rng b2 holds
ex b5 being FinSequence of b1 st
( b4 = b5 & len b5 = b3 ) )
proof end;

definition
let c1 be non empty set ;
let c2, c3 be Nat;
canceled;
mode Matrix of c2,c3,c1 -> Matrix of a1 means :Def3: :: MATRIX_1:def 3
( len a4 = a2 & ( for b1 being FinSequence of a1 st b1 in rng a4 holds
len b1 = a3 ) );
existence
ex b1 being Matrix of c1 st
( len b1 = c2 & ( for b2 being FinSequence of c1 st b2 in rng b1 holds
len b2 = c3 ) )
proof end;
end;

:: deftheorem Def2 MATRIX_1:def 2 :
canceled;

:: deftheorem Def3 defines Matrix MATRIX_1:def 3 :
for b1 being non empty set
for b2, b3 being Nat
for b4 being Matrix of b1 holds
( b4 is Matrix of b2,b3,b1 iff ( len b4 = b2 & ( for b5 being FinSequence of b1 st b5 in rng b4 holds
len b5 = b3 ) ) );

definition
let c1 be non empty set ;
let c2 be Nat;
mode Matrix of a2,a1 is Matrix of a2,a2,a1;
end;

definition
let c1 be non empty 1-sorted ;
mode Matrix of a1 is Matrix of the carrier of a1;
let c2 be Nat;
mode Matrix of a2,a1 is Matrix of a2,a2,the carrier of a1;
let c3 be Nat;
mode Matrix of a2,a3,a1 is Matrix of a2,a3,the carrier of a1;
end;

theorem Th10: :: MATRIX_1:10
for b1, b2 being Nat
for b3 being non empty set
for b4 being Element of b3 holds b1 |-> (b2 |-> b4) is Matrix of b1,b2,b3
proof end;

theorem Th11: :: MATRIX_1:11
for b1 being non empty set
for b2 being FinSequence of b1 holds <*b2*> is Matrix of 1, len b2,b1
proof end;

theorem Th12: :: MATRIX_1:12
for b1 being Nat
for b2 being non empty set
for b3, b4 being FinSequence of b2 st len b3 = b1 & len b4 = b1 holds
<*b3,b4*> is Matrix of 2,b1,b2
proof end;

theorem Th13: :: MATRIX_1:13
for b1 being Nat
for b2 being non empty set holds {} is Matrix of 0,b1,b2
proof end;

theorem Th14: :: MATRIX_1:14
for b1 being non empty set holds <*{} *> is Matrix of 1,0,b1
proof end;

theorem Th15: :: MATRIX_1:15
for b1 being non empty set
for b2 being Element of b1 holds <*<*b2*>*> is Matrix of 1,b1
proof end;

theorem Th16: :: MATRIX_1:16
for b1 being non empty set holds <*{} ,{} *> is Matrix of 2,0,b1
proof end;

theorem Th17: :: MATRIX_1:17
for b1 being non empty set
for b2, b3 being Element of b1 holds <*<*b2,b3*>*> is Matrix of 1,2,b1
proof end;

theorem Th18: :: MATRIX_1:18
for b1 being non empty set
for b2, b3 being Element of b1 holds <*<*b2*>,<*b3*>*> is Matrix of 2,1,b1
proof end;

theorem Th19: :: MATRIX_1:19
for b1 being non empty set
for b2, b3, b4, b5 being Element of b1 holds <*<*b2,b3*>,<*b4,b5*>*> is Matrix of 2,b1
proof end;

definition
let c1 be tabular FinSequence;
func width c1 -> Nat means :Def4: :: MATRIX_1:def 4
ex b1 being FinSequence st
( b1 in rng a1 & len b1 = a2 ) if len a1 > 0
otherwise a2 = 0;
existence
( ( len c1 > 0 implies ex b1 being Natex b2 being FinSequence st
( b2 in rng c1 & len b2 = b1 ) ) & ( not len c1 > 0 implies ex b1 being Nat st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being Nat holds
( ( len c1 > 0 & ex b3 being FinSequence st
( b3 in rng c1 & len b3 = b1 ) & ex b3 being FinSequence st
( b3 in rng c1 & len b3 = b2 ) implies b1 = b2 ) & ( not len c1 > 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof end;
consistency
for b1 being Nat holds verum ;
end;

:: deftheorem Def4 defines width MATRIX_1:def 4 :
for b1 being tabular FinSequence
for b2 being Nat holds
( ( len b1 > 0 implies ( b2 = width b1 iff ex b3 being FinSequence st
( b3 in rng b1 & len b3 = b2 ) ) ) & ( not len b1 > 0 implies ( b2 = width b1 iff b2 = 0 ) ) );

theorem Th20: :: MATRIX_1:20
for b1 being non empty set
for b2 being Matrix of b1 st len b2 > 0 holds
for b3 being Nat holds
( b2 is Matrix of len b2,b3,b1 iff b3 = width b2 )
proof end;

definition
let c1 be tabular FinSequence;
func Indices c1 -> set equals :: MATRIX_1:def 5
[:(dom a1),(Seg (width a1)):];
coherence
[:(dom c1),(Seg (width c1)):] is set ;
end;

:: deftheorem Def5 defines Indices MATRIX_1:def 5 :
for b1 being tabular FinSequence holds Indices b1 = [:(dom b1),(Seg (width b1)):];

definition
let c1 be set ;
let c2 be Matrix of c1;
let c3, c4 be Nat;
assume E15: [c3,c4] in Indices c2 ;
func c2 * c3,c4 -> Element of a1 means :Def6: :: MATRIX_1:def 6
ex b1 being FinSequence of a1 st
( b1 = a2 . a3 & a5 = b1 . a4 );
existence
ex b1 being Element of c1ex b2 being FinSequence of c1 st
( b2 = c2 . c3 & b1 = b2 . c4 )
proof end;
uniqueness
for b1, b2 being Element of c1 st ex b3 being FinSequence of c1 st
( b3 = c2 . c3 & b1 = b3 . c4 ) & ex b3 being FinSequence of c1 st
( b3 = c2 . c3 & b2 = b3 . c4 ) holds
b1 = b2 ;
end;

:: deftheorem Def6 defines * MATRIX_1:def 6 :
for b1 being set
for b2 being Matrix of b1
for b3, b4 being Nat st [b3,b4] in Indices b2 holds
for b5 being Element of b1 holds
( b5 = b2 * b3,b4 iff ex b6 being FinSequence of b1 st
( b6 = b2 . b3 & b5 = b6 . b4 ) );

theorem Th21: :: MATRIX_1:21
for b1 being non empty set
for b2, b3 being Matrix of b1 st len b2 = len b3 & width b2 = width b3 & ( for b4, b5 being Nat st [b4,b5] in Indices b2 holds
b2 * b4,b5 = b3 * b4,b5 ) holds
b2 = b3
proof end;

scheme :: MATRIX_1:sch 1
s1{ F1() -> non empty set , F2() -> Nat, F3() -> Nat, F4( set , set ) -> Element of F1() } :
ex b1 being Matrix of F2(),F3(),F1() st
for b2, b3 being Nat st [b2,b3] in Indices b1 holds
b1 * b2,b3 = F4(b2,b3)
proof end;

scheme :: MATRIX_1:sch 2
s2{ F1() -> non empty set , F2() -> Nat, F3() -> Nat, P1[ set , set , set ] } :
ex b1 being Matrix of F2(),F3(),F1() st
for b2, b3 being Nat st [b2,b3] in Indices b1 holds
P1[b2,b3,b1 * b2,b3]
provided
for b1, b2 being Nat st [b1,b2] in [:(Seg F2()),(Seg F3()):] holds
for b3, b4 being Element of F1() st P1[b1,b2,b3] & P1[b1,b2,b4] holds
b3 = b4 and
E17: for b1, b2 being Nat st [b1,b2] in [:(Seg F2()),(Seg F3()):] holds
ex b3 being Element of F1() st P1[b1,b2,b3]
proof end;

theorem Th22: :: MATRIX_1:22
canceled;

theorem Th23: :: MATRIX_1:23
for b1 being Nat
for b2 being non empty set
for b3 being Matrix of 0,b1,b2 holds
( len b3 = 0 & width b3 = 0 & Indices b3 = {} )
proof end;

theorem Th24: :: MATRIX_1:24
for b1, b2 being Nat
for b3 being non empty set st b1 > 0 holds
for b4 being Matrix of b1,b2,b3 holds
( len b4 = b1 & width b4 = b2 & Indices b4 = [:(Seg b1),(Seg b2):] )
proof end;

theorem Th25: :: MATRIX_1:25
for b1 being Nat
for b2 being non empty set
for b3 being Matrix of b1,b2 holds
( len b3 = b1 & width b3 = b1 & Indices b3 = [:(Seg b1),(Seg b1):] )
proof end;

theorem Th26: :: MATRIX_1:26
for b1, b2 being Nat
for b3 being non empty set
for b4 being Matrix of b1,b2,b3 holds
( len b4 = b1 & Indices b4 = [:(Seg b1),(Seg (width b4)):] )
proof end;

theorem Th27: :: MATRIX_1:27
for b1, b2 being Nat
for b3 being non empty set
for b4, b5 being Matrix of b1,b2,b3 holds Indices b4 = Indices b5
proof end;

theorem Th28: :: MATRIX_1:28
for b1, b2 being Nat
for b3 being non empty set
for b4, b5 being Matrix of b1,b2,b3 st ( for b6, b7 being Nat st [b6,b7] in Indices b4 holds
b4 * b6,b7 = b5 * b6,b7 ) holds
b4 = b5
proof end;

theorem Th29: :: MATRIX_1:29
for b1 being Nat
for b2 being non empty set
for b3 being Matrix of b1,b2
for b4, b5 being Nat st [b4,b5] in Indices b3 holds
[b5,b4] in Indices b3
proof end;

definition
let c1 be non empty set ;
let c2 be Matrix of c1;
func c2 @ -> Matrix of a1 means :: MATRIX_1:def 7
( len a3 = width a2 & ( for b1, b2 being Nat holds
( [b1,b2] in Indices a3 iff [b2,b1] in Indices a2 ) ) & ( for b1, b2 being Nat st [b2,b1] in Indices a2 holds
a3 * b1,b2 = a2 * b2,b1 ) );
existence
ex b1 being Matrix of c1 st
( len b1 = width c2 & ( for b2, b3 being Nat holds
( [b2,b3] in Indices b1 iff [b3,b2] in Indices c2 ) ) & ( for b2, b3 being Nat st [b3,b2] in Indices c2 holds
b1 * b2,b3 = c2 * b3,b2 ) )
proof end;
uniqueness
for b1, b2 being Matrix of c1 st len b1 = width c2 & ( for b3, b4 being Nat holds
( [b3,b4] in Indices b1 iff [b4,b3] in Indices c2 ) ) & ( for b3, b4 being Nat st [b4,b3] in Indices c2 holds
b1 * b3,b4 = c2 * b4,b3 ) & len b2 = width c2 & ( for b3, b4 being Nat holds
( [b3,b4] in Indices b2 iff [b4,b3] in Indices c2 ) ) & ( for b3, b4 being Nat st [b4,b3] in Indices c2 holds
b2 * b3,b4 = c2 * b4,b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines @ MATRIX_1:def 7 :
for b1 being non empty set
for b2, b3 being Matrix of b1 holds
( b3 = b2 @ iff ( len b3 = width b2 & ( for b4, b5 being Nat holds
( [b4,b5] in Indices b3 iff [b5,b4] in Indices b2 ) ) & ( for b4, b5 being Nat st [b5,b4] in Indices b2 holds
b3 * b4,b5 = b2 * b5,b4 ) ) );

definition
let c1 be non empty set ;
let c2 be Matrix of c1;
let c3 be Nat;
func Line c2,c3 -> FinSequence of a1 means :Def8: :: MATRIX_1:def 8
( len a4 = width a2 & ( for b1 being Nat st b1 in Seg (width a2) holds
a4 . b1 = a2 * a3,b1 ) );
existence
ex b1 being FinSequence of c1 st
( len b1 = width c2 & ( for b2 being Nat st b2 in Seg (width c2) holds
b1 . b2 = c2 * c3,b2 ) )
proof end;
uniqueness
for b1, b2 being FinSequence of c1 st len b1 = width c2 & ( for b3 being Nat st b3 in Seg (width c2) holds
b1 . b3 = c2 * c3,b3 ) & len b2 = width c2 & ( for b3 being Nat st b3 in Seg (width c2) holds
b2 . b3 = c2 * c3,b3 ) holds
b1 = b2
proof end;
func Col c2,c3 -> FinSequence of a1 means :Def9: :: MATRIX_1:def 9
( len a4 = len a2 & ( for b1 being Nat st b1 in dom a2 holds
a4 . b1 = a2 * b1,a3 ) );
existence
ex b1 being FinSequence of c1 st
( len b1 = len c2 & ( for b2 being Nat st b2 in dom c2 holds
b1 . b2 = c2 * b2,c3 ) )
proof end;
uniqueness
for b1, b2 being FinSequence of c1 st len b1 = len c2 & ( for b3 being Nat st b3 in dom c2 holds
b1 . b3 = c2 * b3,c3 ) & len b2 = len c2 & ( for b3 being Nat st b3 in dom c2 holds
b2 . b3 = c2 * b3,c3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines Line MATRIX_1:def 8 :
for b1 being non empty set
for b2 being Matrix of b1
for b3 being Nat
for b4 being FinSequence of b1 holds
( b4 = Line b2,b3 iff ( len b4 = width b2 & ( for b5 being Nat st b5 in Seg (width b2) holds
b4 . b5 = b2 * b3,b5 ) ) );

:: deftheorem Def9 defines Col MATRIX_1:def 9 :
for b1 being non empty set
for b2 being Matrix of b1
for b3 being Nat
for b4 being FinSequence of b1 holds
( b4 = Col b2,b3 iff ( len b4 = len b2 & ( for b5 being Nat st b5 in dom b2 holds
b4 . b5 = b2 * b5,b3 ) ) );

definition
let c1 be non empty set ;
let c2 be Matrix of c1;
let c3 be Nat;
redefine func Line as Line c2,c3 -> Element of (width a2) -tuples_on a1;
coherence
Line c2,c3 is Element of (width c2) -tuples_on c1
proof end;
redefine func Col as Col c2,c3 -> Element of (len a2) -tuples_on a1;
coherence
Col c2,c3 is Element of (len c2) -tuples_on c1
proof end;
end;

definition
let c1 be non empty doubleLoopStr ;
let c2 be Nat;
func c2 -Matrices_over c1 -> set equals :: MATRIX_1:def 10
a2 -tuples_on (a2 -tuples_on the carrier of a1);
coherence
c2 -tuples_on (c2 -tuples_on the carrier of c1) is set ;
func 0. c1,c2 -> Matrix of a2,a1 equals :: MATRIX_1:def 11
a2 |-> (a2 |-> (0. a1));
coherence
c2 |-> (c2 |-> (0. c1)) is Matrix of c2,c1 by Th10;
func 1. c1,c2 -> Matrix of a2,a1 means :Def12: :: MATRIX_1:def 12
( ( for b1 being Nat st [b1,b1] in Indices a3 holds
a3 * b1,b1 = 1. a1 ) & ( for b1, b2 being Nat st [b1,b2] in Indices a3 & b1 <> b2 holds
a3 * b1,b2 = 0. a1 ) );
existence
ex b1 being Matrix of c2,c1 st
( ( for b2 being Nat st [b2,b2] in Indices b1 holds
b1 * b2,b2 = 1. c1 ) & ( for b2, b3 being Nat st [b2,b3] in Indices b1 & b2 <> b3 holds
b1 * b2,b3 = 0. c1 ) )
proof end;
uniqueness
for b1, b2 being Matrix of c2,c1 st ( for b3 being Nat st [b3,b3] in Indices b1 holds
b1 * b3,b3 = 1. c1 ) & ( for b3, b4 being Nat st [b3,b4] in Indices b1 & b3 <> b4 holds
b1 * b3,b4 = 0. c1 ) & ( for b3 being Nat st [b3,b3] in Indices b2 holds
b2 * b3,b3 = 1. c1 ) & ( for b3, b4 being Nat st [b3,b4] in Indices b2 & b3 <> b4 holds
b2 * b3,b4 = 0. c1 ) holds
b1 = b2
proof end;
let c3 be Matrix of c2,c1;
func - c3 -> Matrix of a2,a1 means :Def13: :: MATRIX_1:def 13
for b1, b2 being Nat st [b1,b2] in Indices a3 holds
a4 * b1,b2 = - (a3 * b1,b2);
existence
ex b1 being Matrix of c2,c1 st
for b2, b3 being Nat st [b2,b3] in Indices c3 holds
b1 * b2,b3 = - (c3 * b2,b3)
proof end;
uniqueness
for b1, b2 being Matrix of c2,c1 st ( for b3, b4 being Nat st [b3,b4] in Indices c3 holds
b1 * b3,b4 = - (c3 * b3,b4) ) & ( for b3, b4 being Nat st [b3,b4] in Indices c3 holds
b2 * b3,b4 = - (c3 * b3,b4) ) holds
b1 = b2
proof end;
let c4 be Matrix of c2,c1;
func c3 + c4 -> Matrix of a2,a1 means :Def14: :: MATRIX_1:def 14
for b1, b2 being Nat st [b1,b2] in Indices a3 holds
a5 * b1,b2 = (a3 * b1,b2) + (a4 * b1,b2);
existence
ex b1 being Matrix of c2,c1 st
for b2, b3 being Nat st [b2,b3] in Indices c3 holds
b1 * b2,b3 = (c3 * b2,b3) + (c4 * b2,b3)
proof end;
uniqueness
for b1, b2 being Matrix of c2,c1 st ( for b3, b4 being Nat st [b3,b4] in Indices c3 holds
b1 * b3,b4 = (c3 * b3,b4) + (c4 * b3,b4) ) & ( for b3, b4 being Nat st [b3,b4] in Indices c3 holds
b2 * b3,b4 = (c3 * b3,b4) + (c4 * b3,b4) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines -Matrices_over MATRIX_1:def 10 :
for b1 being non empty doubleLoopStr
for b2 being Nat holds b2 -Matrices_over b1 = b2 -tuples_on (b2 -tuples_on the carrier of b1);

:: deftheorem Def11 defines 0. MATRIX_1:def 11 :
for b1 being non empty doubleLoopStr
for b2 being Nat holds 0. b1,b2 = b2 |-> (b2 |-> (0. b1));

:: deftheorem Def12 defines 1. MATRIX_1:def 12 :
for b1 being non empty doubleLoopStr
for b2 being Nat
for b3 being Matrix of b2,b1 holds
( b3 = 1. b1,b2 iff ( ( for b4 being Nat st [b4,b4] in Indices b3 holds
b3 * b4,b4 = 1. b1 ) & ( for b4, b5 being Nat st [b4,b5] in Indices b3 & b4 <> b5 holds
b3 * b4,b5 = 0. b1 ) ) );

:: deftheorem Def13 defines - MATRIX_1:def 13 :
for b1 being non empty doubleLoopStr
for b2 being Nat
for b3, b4 being Matrix of b2,b1 holds
( b4 = - b3 iff for b5, b6 being Nat st [b5,b6] in Indices b3 holds
b4 * b5,b6 = - (b3 * b5,b6) );

:: deftheorem Def14 defines + MATRIX_1:def 14 :
for b1 being non empty doubleLoopStr
for b2 being Nat
for b3, b4, b5 being Matrix of b2,b1 holds
( b5 = b3 + b4 iff for b6, b7 being Nat st [b6,b7] in Indices b3 holds
b5 * b6,b7 = (b3 * b6,b7) + (b4 * b6,b7) );

registration
let c1 be non empty doubleLoopStr ;
let c2 be Nat;
cluster a2 -Matrices_over a1 -> non empty ;
coherence
not c2 -Matrices_over c1 is empty ;
end;

theorem Th30: :: MATRIX_1:30
for b1, b2, b3 being Nat
for b4 being non empty doubleLoopStr st [b1,b2] in Indices (0. b4,b3) holds
(0. b4,b3) * b1,b2 = 0. b4
proof end;

theorem Th31: :: MATRIX_1:31
for b1 being set
for b2 being Nat
for b3 being non empty doubleLoopStr holds
( b1 is Element of b2 -Matrices_over b3 iff b1 is Matrix of b2,b3 )
proof end;

definition
let c1 be non empty doubleLoopStr ;
let c2 be Nat;
mode Diagonal of c2,c1 -> Matrix of a2,a1 means :: MATRIX_1:def 15
for b1, b2 being Nat st [b1,b2] in Indices a3 & a3 * b1,b2 <> 0. a1 holds
b1 = b2;
existence
ex b1 being Matrix of c2,c1 st
for b2, b3 being Nat st [b2,b3] in Indices b1 & b1 * b2,b3 <> 0. c1 holds
b2 = b3
proof end;
end;

:: deftheorem Def15 defines Diagonal MATRIX_1:def 15 :
for b1 being non empty doubleLoopStr
for b2 being Nat
for b3 being Matrix of b2,b1 holds
( b3 is Diagonal of b2,b1 iff for b4, b5 being Nat st [b4,b5] in Indices b3 & b3 * b4,b5 <> 0. b1 holds
b4 = b5 );

theorem Th32: :: MATRIX_1:32
for b1 being Nat
for b2 being non empty Abelian add-associative right_zeroed right_complementable doubleLoopStr
for b3, b4 being Matrix of b1,b2 holds b3 + b4 = b4 + b3
proof end;

theorem Th33: :: MATRIX_1:33
for b1 being Nat
for b2 being non empty Abelian add-associative right_zeroed right_complementable doubleLoopStr
for b3, b4, b5 being Matrix of b1,b2 holds (b3 + b4) + b5 = b3 + (b4 + b5)
proof end;

theorem Th34: :: MATRIX_1:34
for b1 being Nat
for b2 being non empty Abelian add-associative right_zeroed right_complementable doubleLoopStr
for b3 being Matrix of b1,b2 holds b3 + (0. b2,b1) = b3
proof end;

theorem Th35: :: MATRIX_1:35
for b1 being Nat
for b2 being non empty Abelian add-associative right_zeroed right_complementable doubleLoopStr
for b3 being Matrix of b1,b2 holds b3 + (- b3) = 0. b2,b1
proof end;

definition
let c1 be non empty Abelian add-associative right_zeroed right_complementable doubleLoopStr ;
let c2 be Nat;
func c2 -G_Matrix_over c1 -> strict AbGroup means :: MATRIX_1:def 16
( the carrier of a3 = a2 -Matrices_over a1 & ( for b1, b2 being Matrix of a2,a1 holds the add of a3 . b1,b2 = b1 + b2 ) & the Zero of a3 = 0. a1,a2 );
existence
ex b1 being strict AbGroup st
( the carrier of b1 = c2 -Matrices_over c1 & ( for b2, b3 being Matrix of c2,c1 holds the add of b1 . b2,b3 = b2 + b3 ) & the Zero of b1 = 0. c1,c2 )
proof end;
uniqueness
for b1, b2 being strict AbGroup st the carrier of b1 = c2 -Matrices_over c1 & ( for b3, b4 being Matrix of c2,c1 holds the add of b1 . b3,b4 = b3 + b4 ) & the Zero of b1 = 0. c1,c2 & the carrier of b2 = c2 -Matrices_over c1 & ( for b3, b4 being Matrix of c2,c1 holds the add of b2 . b3,b4 = b3 + b4 ) & the Zero of b2 = 0. c1,c2 holds
b1 = b2
proof end;
end;

:: deftheorem Def16 defines -G_Matrix_over MATRIX_1:def 16 :
for b1 being non empty Abelian add-associative right_zeroed right_complementable doubleLoopStr
for b2 being Nat
for b3 being strict AbGroup holds
( b3 = b2 -G_Matrix_over b1 iff ( the carrier of b3 = b2 -Matrices_over b1 & ( for b4, b5 being Matrix of b2,b1 holds the add of b3 . b4,b5 = b4 + b5 ) & the Zero of b3 = 0. b1,b2 ) );