:: MATRIX_3 semantic presentation

begin


definition
let K be Field;
let n, m be Nat;
func 0. (K,n,m) ->  Matrix of n,m,K equals :: MATRIX_3:def 1
n |-> (m |-> (0. K));
coherence
 n |-> (m |-> (0. K)) is Matrix of n,m,K by MATRIX_1:10;
end;

:: deftheorem  defines 0. MATRIX_3:def_1_:_
 for K being Field
for n, m being Nat holds 0. (K,n,m) = n |-> (m |-> (0. K));

definition
let K be Field;
let A be Matrix of K;
func - A ->  Matrix of K means :Def2: :: MATRIX_3:def 2
( len it = len A & width it = width A & ( for i, j being Nat st [i,j] in Indices A holds
it * (i,j) = - (A * (i,j)) ) );
existence
 ex b1 being Matrix of K st
( len b1 = len A & width b1 = width A & ( for i, j being Nat st [i,j] in Indices A holds
b1 * (i,j) = - (A * (i,j)) ) )
proof
set n = len A;
deffunc H1( Nat, Nat) ->  Element of the carrier of K = - (A * ($1,$2));
consider M being Matrix of len A, width A,K such that
A1: for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = H1(i,j) from MATRIX_1:sch_1();
reconsider A1 = A as Matrix of len A, width A,K by MATRIX_2:7;
A2: Indices A1 = [:(Seg (len A)),(Seg (width A)):] by MATRIX_1:25;
A3: now__::_thesis:_(_(_len_A_>_0_&_len_M_=_len_A_&_width_M_=_width_A_&_Indices_A_=_Indices_M_)_or_(_len_A_=_0_&_len_M_=_len_A_&_width_M_=_width_A_&_Indices_A_=_Indices_M_)_)
percases ( len A > 0 or len A = 0 ) ;
case len A > 0 ; ::_thesis: ( len M = len A & width M = width A & Indices A = Indices M )
hence  ( len M = len A & width M = width A & Indices A = Indices M ) by A2, MATRIX_1:23; ::_thesis: verum
end;
caseA4: len A = 0 ; ::_thesis: ( len M = len A & width M = width A & Indices A = Indices M )
then  len M = 0 by MATRIX_1:def_2;
then A5: width M = 0 by MATRIX_1:def_3;
 width A = 0 by A4, MATRIX_1:def_3;
hence  ( len M = len A & width M = width A & Indices A = Indices M ) by A2, A5, MATRIX_1:25; ::_thesis: verum
end;
end;
end;
reconsider M = M as Matrix of K ;
take  M ; ::_thesis: ( len M = len A & width M = width A & ( for i, j being Nat st [i,j] in Indices A holds
M * (i,j) = - (A * (i,j)) ) )
thus  ( len M = len A & width M = width A & ( for i, j being Nat st [i,j] in Indices A holds
M * (i,j) = - (A * (i,j)) ) ) by A1, A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Matrix of K st len b1 = len A & width b1 = width A & ( for i, j being Nat st [i,j] in Indices A holds
b1 * (i,j) = - (A * (i,j)) ) & len b2 = len A & width b2 = width A & ( for i, j being Nat st [i,j] in Indices A holds
b2 * (i,j) = - (A * (i,j)) ) holds
b1 = b2
proof
let M1, M2 be Matrix of K; ::_thesis: ( len M1 = len A & width M1 = width A & ( for i, j being Nat st [i,j] in Indices A holds
M1 * (i,j) = - (A * (i,j)) ) & len M2 = len A & width M2 = width A & ( for i, j being Nat st [i,j] in Indices A holds
M2 * (i,j) = - (A * (i,j)) ) implies M1 = M2 )
set n = len A;
assume that
A6: ( len M1 = len A & width M1 = width A ) and
A7: for i, j being Nat st [i,j] in Indices A holds
M1 * (i,j) = - (A * (i,j)) and
A8: ( len M2 = len A & width M2 = width A ) and
A9: for i, j being Nat st [i,j] in Indices A holds
M2 * (i,j) = - (A * (i,j)) ; ::_thesis: M1 = M2
reconsider M2 = M2 as Matrix of len A, width A,K by A8, MATRIX_2:7;
reconsider M1 = M1 as Matrix of len A, width A,K by A6, MATRIX_2:7;
reconsider A1 = A as Matrix of len A, width A,K by MATRIX_2:7;
A10: Indices A1 = [:(Seg (len A)),(Seg (width A)):] by MATRIX_1:25;
A11: ( Indices M1 = [:(Seg (len A)),(Seg (width M1)):] & Indices M2 = [:(Seg (len A)),(Seg (width M2)):] ) by MATRIX_1:25;
A12: now__::_thesis:_(_(_len_A_>_0_&_Indices_A_=_Indices_M1_&_Indices_M1_=_Indices_M2_)_or_(_len_A_=_0_&_Indices_A_=_Indices_M1_&_Indices_M1_=_Indices_M2_)_)
percases ( len A > 0 or len A = 0 ) ;
caseA13: len A > 0 ; ::_thesis: ( Indices A = Indices M1 & Indices M1 = Indices M2 )
then  Indices M1 = [:(Seg (len A)),(Seg (width A)):] by MATRIX_1:23;
hence  ( Indices A = Indices M1 & Indices M1 = Indices M2 ) by A10, A13, MATRIX_1:23; ::_thesis: verum
end;
caseA14: len A = 0 ; ::_thesis: ( Indices A = Indices M1 & Indices M1 = Indices M2 )
then  len M1 = 0 by MATRIX_1:def_2;
then A15: width M1 = 0 by MATRIX_1:def_3;
 len M2 = 0 by A14, MATRIX_1:def_2;
hence  ( Indices A = Indices M1 & Indices M1 = Indices M2 ) by A10, A11, A14, A15, MATRIX_1:def_3; ::_thesis: verum
end;
end;
end;
now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_A_holds_
M1_*_(i,j)_=_M2_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices A implies M1 * (i,j) = M2 * (i,j) )
assume A16: [i,j] in Indices A ; ::_thesis: M1 * (i,j) = M2 * (i,j)
then  M1 * (i,j) = - (A * (i,j)) by A7;
hence  M1 * (i,j) = M2 * (i,j) by A9, A16; ::_thesis: verum
end;
hence  M1 = M2 by A12, MATRIX_1:27; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines - MATRIX_3:def_2_:_
 for K being Field
for A, b3 being Matrix of K holds
( b3 = - A iff ( len b3 = len A & width b3 = width A & ( for i, j being Nat st [i,j] in Indices A holds
b3 * (i,j) = - (A * (i,j)) ) ) );

definition
let K be Field;
let A, B be Matrix of K;
funcA + B ->  Matrix of K means :Def3: :: MATRIX_3:def 3
( len it = len A & width it = width A & ( for i, j being Nat st [i,j] in Indices A holds
it * (i,j) = (A * (i,j)) + (B * (i,j)) ) );
existence
 ex b1 being Matrix of K st
( len b1 = len A & width b1 = width A & ( for i, j being Nat st [i,j] in Indices A holds
b1 * (i,j) = (A * (i,j)) + (B * (i,j)) ) )
proof
set n = len A;
reconsider A1 = A as Matrix of len A, width A,K by MATRIX_2:7;
deffunc H1( Nat, Nat) ->  Element of the carrier of K = (A * ($1,$2)) + (B * ($1,$2));
consider M being Matrix of len A, width A,K such that
A1: for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = H1(i,j) from MATRIX_1:sch_1();
A2: Indices A1 = [:(Seg (len A)),(Seg (width A)):] by MATRIX_1:25;
A3: now__::_thesis:_(_(_len_A_>_0_&_len_M_=_len_A_&_width_M_=_width_A_&_Indices_A_=_Indices_M_)_or_(_len_A_=_0_&_len_M_=_len_A_&_width_M_=_width_A_&_Indices_A_=_Indices_M_)_)
percases ( len A > 0 or len A = 0 ) ;
case len A > 0 ; ::_thesis: ( len M = len A & width M = width A & Indices A = Indices M )
hence  ( len M = len A & width M = width A & Indices A = Indices M ) by A2, MATRIX_1:23; ::_thesis: verum
end;
caseA4: len A = 0 ; ::_thesis: ( len M = len A & width M = width A & Indices A = Indices M )
then  len M = 0 by MATRIX_1:def_2;
then A5: width M = 0 by MATRIX_1:def_3;
 width A = 0 by A4, MATRIX_1:def_3;
hence  ( len M = len A & width M = width A & Indices A = Indices M ) by A2, A5, MATRIX_1:25; ::_thesis: verum
end;
end;
end;
reconsider M = M as Matrix of K ;
take  M ; ::_thesis: ( len M = len A & width M = width A & ( for i, j being Nat st [i,j] in Indices A holds
M * (i,j) = (A * (i,j)) + (B * (i,j)) ) )
thus  ( len M = len A & width M = width A & ( for i, j being Nat st [i,j] in Indices A holds
M * (i,j) = (A * (i,j)) + (B * (i,j)) ) ) by A1, A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Matrix of K st len b1 = len A & width b1 = width A & ( for i, j being Nat st [i,j] in Indices A holds
b1 * (i,j) = (A * (i,j)) + (B * (i,j)) ) & len b2 = len A & width b2 = width A & ( for i, j being Nat st [i,j] in Indices A holds
b2 * (i,j) = (A * (i,j)) + (B * (i,j)) ) holds
b1 = b2
proof
set n = len A;
let M1, M2 be Matrix of K; ::_thesis: ( len M1 = len A & width M1 = width A & ( for i, j being Nat st [i,j] in Indices A holds
M1 * (i,j) = (A * (i,j)) + (B * (i,j)) ) & len M2 = len A & width M2 = width A & ( for i, j being Nat st [i,j] in Indices A holds
M2 * (i,j) = (A * (i,j)) + (B * (i,j)) ) implies M1 = M2 )
assume that
A6: ( len M1 = len A & width M1 = width A ) and
A7: for i, j being Nat st [i,j] in Indices A holds
M1 * (i,j) = (A * (i,j)) + (B * (i,j)) and
A8: ( len M2 = len A & width M2 = width A ) and
A9: for i, j being Nat st [i,j] in Indices A holds
M2 * (i,j) = (A * (i,j)) + (B * (i,j)) ; ::_thesis: M1 = M2
reconsider M2 = M2 as Matrix of len A, width A,K by A8, MATRIX_2:7;
reconsider M1 = M1 as Matrix of len A, width A,K by A6, MATRIX_2:7;
reconsider A1 = A as Matrix of len A, width A,K by MATRIX_2:7;
A10: Indices A1 = [:(Seg (len A)),(Seg (width A)):] by MATRIX_1:25;
A11: ( Indices M1 = [:(Seg (len A)),(Seg (width M1)):] & Indices M2 = [:(Seg (len A)),(Seg (width M2)):] ) by MATRIX_1:25;
A12: now__::_thesis:_(_(_len_A_>_0_&_Indices_A_=_Indices_M1_&_Indices_M1_=_Indices_M2_)_or_(_len_A_=_0_&_Indices_A_=_Indices_M1_&_Indices_M1_=_Indices_M2_)_)
percases ( len A > 0 or len A = 0 ) ;
caseA13: len A > 0 ; ::_thesis: ( Indices A = Indices M1 & Indices M1 = Indices M2 )
then  Indices M1 = [:(Seg (len A)),(Seg (width A)):] by MATRIX_1:23;
hence  ( Indices A = Indices M1 & Indices M1 = Indices M2 ) by A10, A13, MATRIX_1:23; ::_thesis: verum
end;
caseA14: len A = 0 ; ::_thesis: ( Indices A = Indices M1 & Indices M1 = Indices M2 )
then  len M1 = 0 by MATRIX_1:def_2;
then A15: width M1 = 0 by MATRIX_1:def_3;
 len M2 = 0 by A14, MATRIX_1:def_2;
hence  ( Indices A = Indices M1 & Indices M1 = Indices M2 ) by A10, A11, A14, A15, MATRIX_1:def_3; ::_thesis: verum
end;
end;
end;
now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_A_holds_
M1_*_(i,j)_=_M2_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices A implies M1 * (i,j) = M2 * (i,j) )
assume A16: [i,j] in Indices A ; ::_thesis: M1 * (i,j) = M2 * (i,j)
then  M1 * (i,j) = (A * (i,j)) + (B * (i,j)) by A7;
hence  M1 * (i,j) = M2 * (i,j) by A9, A16; ::_thesis: verum
end;
hence  M1 = M2 by A12, MATRIX_1:27; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines + MATRIX_3:def_3_:_
 for K being Field
for A, B, b4 being Matrix of K holds
( b4 = A + B iff ( len b4 = len A & width b4 = width A & ( for i, j being Nat st [i,j] in Indices A holds
b4 * (i,j) = (A * (i,j)) + (B * (i,j)) ) ) );

theorem Th1: :: MATRIX_3:1
for n, m being Nat
for K being Field
for i, j being Nat st [i,j] in Indices (0. (K,n,m)) holds
(0. (K,n,m)) * (i,j) = 0. K
proof
let n, m be Nat; ::_thesis: for K being Field
for i, j being Nat st [i,j] in Indices (0. (K,n,m)) holds
(0. (K,n,m)) * (i,j) = 0. K
let K be Field; ::_thesis: for i, j being Nat st [i,j] in Indices (0. (K,n,m)) holds
(0. (K,n,m)) * (i,j) = 0. K
let i, j be Nat; ::_thesis: ( [i,j] in Indices (0. (K,n,m)) implies (0. (K,n,m)) * (i,j) = 0. K )
assume A1: [i,j] in Indices (0. (K,n,m)) ; ::_thesis: (0. (K,n,m)) * (i,j) = 0. K
A2: Indices (0. (K,n,m)) = [:(Seg n),(Seg (width (0. (K,n,m)))):] by MATRIX_1:25;
percases ( n > 0 or n = 0 ) ;
supposeA3: n > 0 ; ::_thesis: (0. (K,n,m)) * (i,j) = 0. K
reconsider m1 = m as Element of NAT by ORDINAL1:def_12;
A4: [i,j] in [:(Seg n),(Seg m):] by A1, A3, MATRIX_1:23;
then  j in Seg m by ZFMISC_1:87;
then A5: (m1 |-> (0. K)) . j = 0. K by FUNCOP_1:7;
 i in Seg n by A4, ZFMISC_1:87;
then  (0. (K,n,m)) . i = m |-> (0. K) by FUNCOP_1:7;
hence  (0. (K,n,m)) * (i,j) = 0. K by A1, A5, MATRIX_1:def_5; ::_thesis: verum
end;
suppose n = 0 ; ::_thesis: (0. (K,n,m)) * (i,j) = 0. K
then  Seg n = {} ;
hence  (0. (K,n,m)) * (i,j) = 0. K by A1, A2, ZFMISC_1:90; ::_thesis: verum
end;
end;
end;

theorem :: MATRIX_3:2
for K being Field
for A, B being Matrix of K st len A = len B & width A = width B holds
A + B = B + A
proof
let K be Field; ::_thesis: for A, B being Matrix of K st len A = len B & width A = width B holds
A + B = B + A
let A, B be Matrix of K; ::_thesis: ( len A = len B & width A = width B implies A + B = B + A )
assume that
A1: len A = len B and
A2: width A = width B ; ::_thesis: A + B = B + A
A3: width A = width (A + B) by Def3;
then A4: width (A + B) = width (B + A) by A2, Def3;
A5: len A = len (A + B) by Def3;
then  dom A = dom (A + B) by FINSEQ_3:29;
then A6: Indices A = Indices (A + B) by A3;
 dom A = dom B by A1, FINSEQ_3:29;
then A7: Indices B = [:(dom A),(Seg (width A)):] by A2;
A8: now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_(A_+_B)_holds_
(A_+_B)_*_(i,j)_=_(B_+_A)_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices (A + B) implies (A + B) * (i,j) = (B + A) * (i,j) )
assume A9: [i,j] in Indices (A + B) ; ::_thesis: (A + B) * (i,j) = (B + A) * (i,j)
hence (A + B) * (i,j) = (B * (i,j)) + (A * (i,j)) by A6, Def3
.= (B + A) * (i,j) by A7, A6, A9, Def3 ;
::_thesis: verum
end;
 len (A + B) = len (B + A) by A1, A5, Def3;
hence  A + B = B + A by A4, A8, MATRIX_1:21; ::_thesis: verum
end;

theorem :: MATRIX_3:3
for K being Field
for A, B, C being Matrix of K st len A = len B & width A = width B holds
(A + B) + C = A + (B + C)
proof
let K be Field; ::_thesis: for A, B, C being Matrix of K st len A = len B & width A = width B holds
(A + B) + C = A + (B + C)
let A, B, C be Matrix of K; ::_thesis: ( len A = len B & width A = width B implies (A + B) + C = A + (B + C) )
assume that
A1: len A = len B and
A2: width A = width B ; ::_thesis: (A + B) + C = A + (B + C)
 dom A = dom B by A1, FINSEQ_3:29;
then A3: Indices B = [:(dom A),(Seg (width A)):] by A2;
A4: Indices A = [:(dom A),(Seg (width A)):] ;
A5: width ((A + B) + C) = width (A + B) by Def3;
A6: width (A + B) = width A by Def3;
A7: ( len (A + (B + C)) = len A & width (A + (B + C)) = width A ) by Def3;
A8: len (A + B) = len A by Def3;
A9: len ((A + B) + C) = len (A + B) by Def3;
then  dom A = dom ((A + B) + C) by A8, FINSEQ_3:29;
then A10: Indices ((A + B) + C) = [:(dom A),(Seg (width A)):] by A6, A5;
 dom A = dom (A + B) by A8, FINSEQ_3:29;
then A11: Indices (A + B) = [:(dom A),(Seg (width A)):] by A6;
now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_((A_+_B)_+_C)_holds_
((A_+_B)_+_C)_*_(i,j)_=_(A_+_(B_+_C))_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices ((A + B) + C) implies ((A + B) + C) * (i,j) = (A + (B + C)) * (i,j) )
assume A12: [i,j] in Indices ((A + B) + C) ; ::_thesis: ((A + B) + C) * (i,j) = (A + (B + C)) * (i,j)
hence ((A + B) + C) * (i,j) = ((A + B) * (i,j)) + (C * (i,j)) by A11, A10, Def3
.= ((A * (i,j)) + (B * (i,j))) + (C * (i,j)) by A4, A10, A12, Def3
.= (A * (i,j)) + ((B * (i,j)) + (C * (i,j))) by RLVECT_1:def_3
.= (A * (i,j)) + ((B + C) * (i,j)) by A3, A10, A12, Def3
.= (A + (B + C)) * (i,j) by A4, A10, A12, Def3 ;
::_thesis: verum
end;
hence  (A + B) + C = A + (B + C) by A8, A6, A9, A5, A7, MATRIX_1:21; ::_thesis: verum
end;

theorem :: MATRIX_3:4
for n, m being Nat
for K being Field
for A being Matrix of n,m,K holds A + (0. (K,n,m)) = A
proof
let n, m be Nat; ::_thesis: for K being Field
for A being Matrix of n,m,K holds A + (0. (K,n,m)) = A
let K be Field; ::_thesis: for A being Matrix of n,m,K holds A + (0. (K,n,m)) = A
let A be Matrix of n,m,K; ::_thesis: A + (0. (K,n,m)) = A
percases ( n > 0 or n = 0 ) ;
supposeA1: n > 0 ; ::_thesis: A + (0. (K,n,m)) = A
A2: width A = width (A + (0. (K,n,m))) by Def3;
A3: Indices A = [:(Seg n),(Seg m):] by A1, MATRIX_1:23;
A4: len A = len (A + (0. (K,n,m))) by Def3;
then  dom A = dom (A + (0. (K,n,m))) by FINSEQ_3:29;
then A5: Indices A = Indices (A + (0. (K,n,m))) by A2;
A6: Indices (0. (K,n,m)) = [:(Seg n),(Seg m):] by A1, MATRIX_1:23;
now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_(A_+_(0._(K,n,m)))_holds_
(A_+_(0._(K,n,m)))_*_(i,j)_=_A_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices (A + (0. (K,n,m))) implies (A + (0. (K,n,m))) * (i,j) = A * (i,j) )
assume A7: [i,j] in Indices (A + (0. (K,n,m))) ; ::_thesis: (A + (0. (K,n,m))) * (i,j) = A * (i,j)
hence (A + (0. (K,n,m))) * (i,j) = (A * (i,j)) + ((0. (K,n,m)) * (i,j)) by A5, Def3
.= (A * (i,j)) + (0. K) by A3, A6, A5, A7, Th1
.= A * (i,j) by RLVECT_1:4 ;
::_thesis: verum
end;
hence  A + (0. (K,n,m)) = A by A4, A2, MATRIX_1:21; ::_thesis: verum
end;
supposeA8: n = 0 ; ::_thesis: A + (0. (K,n,m)) = A
A9: width A = width (A + (0. (K,n,m))) by Def3;
A10: len A = len (A + (0. (K,n,m))) by Def3;
then  dom A = dom (A + (0. (K,n,m))) by FINSEQ_3:29;
then  ( Indices A = [:(dom A),(Seg (width A)):] & Indices (A + (0. (K,n,m))) = [:(dom A),(Seg (width A)):] ) by A9;
then  for i, j being Nat st [i,j] in Indices (A + (0. (K,n,m))) holds
(A + (0. (K,n,m))) * (i,j) = A * (i,j) by A8, MATRIX_1:22;
hence  A + (0. (K,n,m)) = A by A10, A9, MATRIX_1:21; ::_thesis: verum
end;
end;
end;

theorem :: MATRIX_3:5
for n, m being Nat
for K being Field
for A being Matrix of n,m,K holds A + (- A) = 0. (K,n,m)
proof
let n, m be Nat; ::_thesis: for K being Field
for A being Matrix of n,m,K holds A + (- A) = 0. (K,n,m)
let K be Field; ::_thesis: for A being Matrix of n,m,K holds A + (- A) = 0. (K,n,m)
let A be Matrix of n,m,K; ::_thesis: A + (- A) = 0. (K,n,m)
A1: width (- A) = width A by Def2;
A2: len (A + (- A)) = len A by Def3;
A3: width (A + (- A)) = width A by Def3;
A4: len (- A) = len A by Def2;
A5: now__::_thesis:_(_(_n_>_0_&_len_(0._(K,n,m))_=_len_(A_+_(-_A))_&_width_(0._(K,n,m))_=_width_(A_+_(-_A))_&_Indices_A_=_Indices_(-_A)_&_Indices_A_=_Indices_(A_+_(-_A))_)_or_(_n_=_0_&_len_(0._(K,n,m))_=_len_(A_+_(-_A))_&_width_(0._(K,n,m))_=_width_(A_+_(-_A))_&_Indices_A_=_Indices_(-_A)_&_Indices_A_=_Indices_(A_+_(-_A))_)_)
percases ( n > 0 or n = 0 ) ;
caseA6: n > 0 ; ::_thesis: ( len (0. (K,n,m)) = len (A + (- A)) & width (0. (K,n,m)) = width (A + (- A)) & Indices A = Indices (- A) & Indices A = Indices (A + (- A)) )
then  ( len (A + (- A)) = n & width (A + (- A)) = m ) by A2, A3, MATRIX_1:23;
hence  ( len (0. (K,n,m)) = len (A + (- A)) & width (0. (K,n,m)) = width (A + (- A)) ) by A6, MATRIX_1:23; ::_thesis: ( Indices A = Indices (- A) & Indices A = Indices (A + (- A)) )
 ( dom A = dom (- A) & dom A = dom (A + (- A)) ) by A4, A2, FINSEQ_3:29;
hence  ( Indices A = Indices (- A) & Indices A = Indices (A + (- A)) ) by A1, A3; ::_thesis: verum
end;
caseA7: n = 0 ; ::_thesis: ( len (0. (K,n,m)) = len (A + (- A)) & width (0. (K,n,m)) = width (A + (- A)) & Indices A = Indices (- A) & Indices A = Indices (A + (- A)) )
then A8: width A = 0 by MATRIX_1:22;
then A9: Seg (width (- A)) = Seg 0 by A1;
A10: len A = 0 by A7, MATRIX_1:22;
then A11: dom (- A) = Seg 0 by A4, FINSEQ_1:def_3;
A12: Indices (- A) = [:(dom (- A)),(Seg (width (- A))):]
.= [:(Seg 0),(Seg (width (- A))):] by A11
.= [:(Seg 0),(Seg 0):] by A9 ;
 dom (A + (- A)) = Seg 0 by A2, A10, FINSEQ_1:def_3;
then A13: Indices (A + (- A)) = [:(Seg 0),(Seg 0):] by A3, A8;
 ( len (0. (K,n,m)) = 0 & width (0. (K,n,m)) = 0 ) by A7, MATRIX_1:22;
hence  ( len (0. (K,n,m)) = len (A + (- A)) & width (0. (K,n,m)) = width (A + (- A)) ) by A10, A8, Def3; ::_thesis: ( Indices A = Indices (- A) & Indices A = Indices (A + (- A)) )
 Indices A = {} by A7, MATRIX_1:22;
hence  ( Indices A = Indices (- A) & Indices A = Indices (A + (- A)) ) by A12, A13, ZFMISC_1:90; ::_thesis: verum
end;
end;
end;
A14: Indices A = Indices (0. (K,n,m)) by MATRIX_1:26;
now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_A_holds_
(A_+_(-_A))_*_(i,j)_=_(0._(K,n,m))_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices A implies (A + (- A)) * (i,j) = (0. (K,n,m)) * (i,j) )
assume A15: [i,j] in Indices A ; ::_thesis: (A + (- A)) * (i,j) = (0. (K,n,m)) * (i,j)
hence (A + (- A)) * (i,j) = (A * (i,j)) + ((- A) * (i,j)) by Def3
.= (A * (i,j)) + (- (A * (i,j))) by A15, Def2
.= 0. K by RLVECT_1:5
.= (0. (K,n,m)) * (i,j) by A14, A15, Th1 ;
::_thesis: verum
end;
hence  A + (- A) = 0. (K,n,m) by A5, MATRIX_1:21; ::_thesis: verum
end;

definition
let K be Field;
let A, B be Matrix of K;
assume A1: width A = len B ;
funcA * B ->  Matrix of K means :Def4: :: MATRIX_3:def 4
( len it = len A & width it = width B & ( for i, j being Nat st [i,j] in Indices it holds
it * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) );
existence
 ex b1 being Matrix of K st
( len b1 = len A & width b1 = width B & ( for i, j being Nat st [i,j] in Indices b1 holds
b1 * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) )
proof
deffunc H1( Nat, Nat) ->  Element of the carrier of K = (Line (A,$1)) "*" (Col (B,$2));
consider M being Matrix of len A, width B,K such that
A2: for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = H1(i,j) from MATRIX_1:sch_1();
take  M ; ::_thesis: ( len M = len A & width M = width B & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) )
now__::_thesis:_(_(_len_A_>_0_&_len_M_=_len_A_&_width_M_=_width_B_)_or_(_len_A_=_0_&_len_M_=_len_A_&_width_M_=_width_B_)_)
percases ( len A > 0 or len A = 0 ) ;
case len A > 0 ; ::_thesis: ( len M = len A & width M = width B )
hence  ( len M = len A & width M = width B ) by MATRIX_1:23; ::_thesis: verum
end;
caseA3: len A = 0 ; ::_thesis: ( len M = len A & width M = width B )
then  len B = 0 by A1, MATRIX_1:def_3;
then A4: width B = 0 by MATRIX_1:def_3;
 len M = 0 by A3, MATRIX_1:25;
hence  ( len M = len A & width M = width B ) by A3, A4, MATRIX_1:def_3; ::_thesis: verum
end;
end;
end;
hence  ( len M = len A & width M = width B & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) ) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Matrix of K st len b1 = len A & width b1 = width B & ( for i, j being Nat st [i,j] in Indices b1 holds
b1 * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) & len b2 = len A & width b2 = width B & ( for i, j being Nat st [i,j] in Indices b2 holds
b2 * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) holds
b1 = b2
proof
let M1, M2 be Matrix of K; ::_thesis: ( len M1 = len A & width M1 = width B & ( for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) & len M2 = len A & width M2 = width B & ( for i, j being Nat st [i,j] in Indices M2 holds
M2 * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) implies M1 = M2 )
assume that
A5: len M1 = len A and
A6: width M1 = width B and
A7: for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = (Line (A,i)) "*" (Col (B,j)) and
A8: len M2 = len A and
A9: width M2 = width B and
A10: for i, j being Nat st [i,j] in Indices M2 holds
M2 * (i,j) = (Line (A,i)) "*" (Col (B,j)) ; ::_thesis: M1 = M2
 dom M2 = dom M1 by A5, A8, FINSEQ_3:29;
then A11: ( Indices M1 = [:(dom M1),(Seg (width M1)):] & Indices M2 = [:(dom M1),(Seg (width M1)):] ) by A6, A9;
now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_M1_holds_
M1_*_(i,j)_=_M2_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )
assume A12: [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j)
then  M1 * (i,j) = (Line (A,i)) "*" (Col (B,j)) by A7;
hence  M1 * (i,j) = M2 * (i,j) by A10, A11, A12; ::_thesis: verum
end;
hence  M1 = M2 by A5, A6, A8, A9, MATRIX_1:21; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines * MATRIX_3:def_4_:_
 for K being Field
for A, B being Matrix of K st width A = len B holds
for b4 being Matrix of K holds
( b4 = A * B iff ( len b4 = len A & width b4 = width B & ( for i, j being Nat st [i,j] in Indices b4 holds
b4 * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) ) );

definition
let n, k, m be Nat;
let K be Field;
let A be Matrix of n,k,K;
let B be Matrix of width A,m,K;
:: original: *
redefine funcA * B ->  Matrix of len A, width B,K;
coherence
 A * B is Matrix of len A, width B,K
proof
 width A = len B by MATRIX_1:25;
then  ( len (A * B) = len A & width (A * B) = width B ) by Def4;
hence  A * B is Matrix of len A, width B,K by MATRIX_2:7; ::_thesis: verum
end;
end;

definition
let K be Field;
let M be Matrix of K;
let a be Element of K;
funca * M ->  Matrix of K means :: MATRIX_3:def 5
( len it = len M & width it = width M & ( for i, j being Nat st [i,j] in Indices M holds
it * (i,j) = a * (M * (i,j)) ) );
existence
 ex b1 being Matrix of K st
( len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b1 * (i,j) = a * (M * (i,j)) ) )
proof
deffunc H1( Nat, Nat) ->  Element of the carrier of K = a * (M * ($1,$2));
consider N being Matrix of len M, width M,K such that
A1: for i, j being Nat st [i,j] in Indices N holds
N * (i,j) = H1(i,j) from MATRIX_1:sch_1();
take  N ; ::_thesis: ( len N = len M & width N = width M & ( for i, j being Nat st [i,j] in Indices M holds
N * (i,j) = a * (M * (i,j)) ) )
A2: len N = len M by MATRIX_1:def_2;
A3: now__::_thesis:_(_(_len_M_=_0_&_width_N_=_width_M_)_or_(_len_M_>_0_&_width_N_=_width_M_)_)
percases ( len M = 0 or len M > 0 ) ;
caseA4: len M = 0 ; ::_thesis: width N = width M
then  width N = 0 by A2, MATRIX_1:def_3;
hence  width N = width M by A4, MATRIX_1:def_3; ::_thesis: verum
end;
case len M > 0 ; ::_thesis: width N = width M
hence  width N = width M by MATRIX_1:23; ::_thesis: verum
end;
end;
end;
 dom M = dom N by A2, FINSEQ_3:29;
then  Indices N = [:(dom M),(Seg (width M)):] by A3;
hence  ( len N = len M & width N = width M & ( for i, j being Nat st [i,j] in Indices M holds
N * (i,j) = a * (M * (i,j)) ) ) by A1, A3, MATRIX_1:def_2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Matrix of K st len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b1 * (i,j) = a * (M * (i,j)) ) & len b2 = len M & width b2 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b2 * (i,j) = a * (M * (i,j)) ) holds
b1 = b2
proof
let A, B be Matrix of K; ::_thesis: ( len A = len M & width A = width M & ( for i, j being Nat st [i,j] in Indices M holds
A * (i,j) = a * (M * (i,j)) ) & len B = len M & width B = width M & ( for i, j being Nat st [i,j] in Indices M holds
B * (i,j) = a * (M * (i,j)) ) implies A = B )
assume that
A5: len A = len M and
A6: width A = width M and
A7: for i, j being Nat st [i,j] in Indices M holds
A * (i,j) = a * (M * (i,j)) and
A8: ( len B = len M & width B = width M ) and
A9: for i, j being Nat st [i,j] in Indices M holds
B * (i,j) = a * (M * (i,j)) ; ::_thesis: A = B
now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_A_holds_
A_*_(i,j)_=_B_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices A implies A * (i,j) = B * (i,j) )
 dom A = dom M by A5, FINSEQ_3:29;
then A10: Indices A = [:(dom M),(Seg (width M)):] by A6;
assume A11: [i,j] in Indices A ; ::_thesis: A * (i,j) = B * (i,j)
hence A * (i,j) = a * (M * (i,j)) by A7, A10
.= B * (i,j) by A9, A11, A10 ;
::_thesis: verum
end;
hence  A = B by A5, A6, A8, MATRIX_1:21; ::_thesis: verum
end;
end;

:: deftheorem  defines * MATRIX_3:def_5_:_
 for K being Field
for M being Matrix of K
for a being Element of K
for b4 being Matrix of K holds
( b4 = a * M iff ( len b4 = len M & width b4 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b4 * (i,j) = a * (M * (i,j)) ) ) );

definition
let K be Field;
let M be Matrix of K;
let a be Element of K;
funcM * a ->  Matrix of K equals :: MATRIX_3:def 6
a * M;
coherence
 a * M is Matrix of K ;
end;

:: deftheorem  defines * MATRIX_3:def_6_:_
 for K being Field
for M being Matrix of K
for a being Element of K holds M * a = a * M;

theorem :: MATRIX_3:6
for K being Field
for p, q being FinSequence of K st len p = len q holds
( len (mlt (p,q)) = len p & len (mlt (p,q)) = len q )
proof
let K be Field; ::_thesis: for p, q being FinSequence of K st len p = len q holds
( len (mlt (p,q)) = len p & len (mlt (p,q)) = len q )
let p, q be FinSequence of K; ::_thesis: ( len p = len q implies ( len (mlt (p,q)) = len p & len (mlt (p,q)) = len q ) )
reconsider r = mlt (p,q) as FinSequence of K ;
A1: r = the multF of K .: (p,q) by FVSUM_1:def_7;
assume  len p = len q ; ::_thesis: ( len (mlt (p,q)) = len p & len (mlt (p,q)) = len q )
hence  ( len (mlt (p,q)) = len p & len (mlt (p,q)) = len q ) by A1, FINSEQ_2:72; ::_thesis: verum
end;

theorem :: MATRIX_3:7
for n being Nat
for K being Field
for i, l being Nat st [i,l] in Indices (1. (K,n)) & l = i holds
(Line ((1. (K,n)),i)) . l = 1. K
proof
let n be Nat; ::_thesis: for K being Field
for i, l being Nat st [i,l] in Indices (1. (K,n)) & l = i holds
(Line ((1. (K,n)),i)) . l = 1. K
let K be Field; ::_thesis: for i, l being Nat st [i,l] in Indices (1. (K,n)) & l = i holds
(Line ((1. (K,n)),i)) . l = 1. K
let i, l be Nat; ::_thesis: ( [i,l] in Indices (1. (K,n)) & l = i implies (Line ((1. (K,n)),i)) . l = 1. K )
assume that
A1: [i,l] in Indices (1. (K,n)) and
A2: l = i ; ::_thesis: (Line ((1. (K,n)),i)) . l = 1. K
 l in Seg (width (1. (K,n))) by A1, ZFMISC_1:87;
hence (Line ((1. (K,n)),i)) . l = (1. (K,n)) * (i,l) by MATRIX_1:def_7
.= 1. K by A1, A2, MATRIX_1:def_11 ;
::_thesis: verum
end;

theorem :: MATRIX_3:8
for n being Nat
for K being Field
for i, l being Nat st [i,l] in Indices (1. (K,n)) & l <> i holds
(Line ((1. (K,n)),i)) . l = 0. K
proof
let n be Nat; ::_thesis: for K being Field
for i, l being Nat st [i,l] in Indices (1. (K,n)) & l <> i holds
(Line ((1. (K,n)),i)) . l = 0. K
let K be Field; ::_thesis: for i, l being Nat st [i,l] in Indices (1. (K,n)) & l <> i holds
(Line ((1. (K,n)),i)) . l = 0. K
let i, l be Nat; ::_thesis: ( [i,l] in Indices (1. (K,n)) & l <> i implies (Line ((1. (K,n)),i)) . l = 0. K )
assume that
A1: [i,l] in Indices (1. (K,n)) and
A2: l <> i ; ::_thesis: (Line ((1. (K,n)),i)) . l = 0. K
 l in Seg (width (1. (K,n))) by A1, ZFMISC_1:87;
hence (Line ((1. (K,n)),i)) . l = (1. (K,n)) * (i,l) by MATRIX_1:def_7
.= 0. K by A1, A2, MATRIX_1:def_11 ;
::_thesis: verum
end;

theorem :: MATRIX_3:9
for n being Nat
for K being Field
for l, j being Nat st [l,j] in Indices (1. (K,n)) & l = j holds
(Col ((1. (K,n)),j)) . l = 1. K
proof
let n be Nat; ::_thesis: for K being Field
for l, j being Nat st [l,j] in Indices (1. (K,n)) & l = j holds
(Col ((1. (K,n)),j)) . l = 1. K
let K be Field; ::_thesis: for l, j being Nat st [l,j] in Indices (1. (K,n)) & l = j holds
(Col ((1. (K,n)),j)) . l = 1. K
let l, j be Nat; ::_thesis: ( [l,j] in Indices (1. (K,n)) & l = j implies (Col ((1. (K,n)),j)) . l = 1. K )
assume that
A1: [l,j] in Indices (1. (K,n)) and
A2: l = j ; ::_thesis: (Col ((1. (K,n)),j)) . l = 1. K
 l in dom (1. (K,n)) by A1, ZFMISC_1:87;
hence (Col ((1. (K,n)),j)) . l = (1. (K,n)) * (l,j) by MATRIX_1:def_8
.= 1. K by A1, A2, MATRIX_1:def_11 ;
::_thesis: verum
end;

theorem :: MATRIX_3:10
for n being Nat
for K being Field
for l, j being Nat st [l,j] in Indices (1. (K,n)) & l <> j holds
(Col ((1. (K,n)),j)) . l = 0. K
proof
let n be Nat; ::_thesis: for K being Field
for l, j being Nat st [l,j] in Indices (1. (K,n)) & l <> j holds
(Col ((1. (K,n)),j)) . l = 0. K
let K be Field; ::_thesis: for l, j being Nat st [l,j] in Indices (1. (K,n)) & l <> j holds
(Col ((1. (K,n)),j)) . l = 0. K
let l, j be Nat; ::_thesis: ( [l,j] in Indices (1. (K,n)) & l <> j implies (Col ((1. (K,n)),j)) . l = 0. K )
assume that
A1: [l,j] in Indices (1. (K,n)) and
A2: l <> j ; ::_thesis: (Col ((1. (K,n)),j)) . l = 0. K
 l in dom (1. (K,n)) by A1, ZFMISC_1:87;
hence (Col ((1. (K,n)),j)) . l = (1. (K,n)) * (l,j) by MATRIX_1:def_8
.= 0. K by A1, A2, MATRIX_1:def_11 ;
::_thesis: verum
end;

Lm1:  for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being FinSequence of L st ( for i being Element of NAT st i in dom p holds
p . i = 0. L ) holds
Sum p = 0. L
proof
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being FinSequence of L st ( for i being Element of NAT st i in dom p holds
p . i = 0. L ) holds
Sum p = 0. L
let p be FinSequence of L; ::_thesis: ( ( for i being Element of NAT st i in dom p holds
p . i = 0. L ) implies Sum p = 0. L )
assume A1: for k being Element of NAT st k in dom p holds
p . k = 0. L ; ::_thesis: Sum p = 0. L
defpred S1[ FinSequence of L] means ( ( for k being Element of NAT st k in dom $1 holds
$1 . k = 0. L ) implies Sum $1 = 0. L );
A2: for p being FinSequence of L
for x being Element of L st S1[p] holds
S1[p ^ <*x*>]
proof
let p be FinSequence of L; ::_thesis: for x being Element of L st S1[p] holds
S1[p ^ <*x*>]
let x be Element of L; ::_thesis: ( S1[p] implies S1[p ^ <*x*>] )
assume A3: ( ( for k being Element of NAT st k in dom p holds
p . k = 0. L ) implies Sum p = 0. L ) ; ::_thesis: S1[p ^ <*x*>]
A4: (len p) + 1 in Seg ((len p) + 1) by FINSEQ_1:4;
assume A5: for k being Element of NAT st k in dom (p ^ <*x*>) holds
(p ^ <*x*>) . k = 0. L ; ::_thesis: Sum (p ^ <*x*>) = 0. L
A6: for k being Element of NAT st k in dom p holds
p . k = 0. L
proof
A7: dom p c= dom (p ^ <*x*>) by FINSEQ_1:26;
let k be Element of NAT ; ::_thesis: ( k in dom p implies p . k = 0. L )
assume A8: k in dom p ; ::_thesis: p . k = 0. L
thus p . k = (p ^ <*x*>) . k by A8, FINSEQ_1:def_7
.= 0. L by A5, A8, A7 ; ::_thesis: verum
end;
len (p ^ <*x*>) = (len p) + (len <*x*>) by FINSEQ_1:22
.= (len p) + 1 by FINSEQ_1:39 ;
then A9: (len p) + 1 in dom (p ^ <*x*>) by A4, FINSEQ_1:def_3;
A10: x = (p ^ <*x*>) . ((len p) + 1) by FINSEQ_1:42;
thus  Sum (p ^ <*x*>) = (Sum p) + (Sum <*x*>) by RLVECT_1:41
.= (Sum p) + x by RLVECT_1:44
.= (0. L) + (0. L) by A3, A5, A6, A9, A10
.= 0. L by RLVECT_1:def_4 ; ::_thesis: verum
end;
A11: S1[ <*> the carrier of L] by RLVECT_1:43;
 for p being FinSequence of L holds S1[p] from FINSEQ_2:sch_2(A11, A2);
hence  Sum p = 0. L by A1; ::_thesis: verum
end;

theorem Th11: :: MATRIX_3:11
for n being Element of NAT
for K being non empty right_complementable add-associative right_zeroed addLoopStr holds Sum (n |-> (0. K)) = 0. K
proof
let n be Element of NAT ; ::_thesis: for K being non empty right_complementable add-associative right_zeroed addLoopStr holds Sum (n |-> (0. K)) = 0. K
let K be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: Sum (n |-> (0. K)) = 0. K
set p = n |-> (0. K);
 for i being Element of NAT st i in dom (n |-> (0. K)) holds
(n |-> (0. K)) . i = 0. K
proof
let i be Element of NAT ; ::_thesis: ( i in dom (n |-> (0. K)) implies (n |-> (0. K)) . i = 0. K )
assume  i in dom (n |-> (0. K)) ; ::_thesis: (n |-> (0. K)) . i = 0. K
then  i in Seg n by FUNCOP_1:13;
hence  (n |-> (0. K)) . i = 0. K by FUNCOP_1:7; ::_thesis: verum
end;
hence  Sum (n |-> (0. K)) = 0. K by Lm1; ::_thesis: verum
end;

theorem Th12: :: MATRIX_3:12
for K being non empty right_complementable add-associative right_zeroed addLoopStr
for p being FinSequence of K
for i being Nat st i in dom p & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) holds
Sum p = p . i
proof
let K be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being FinSequence of K
for i being Nat st i in dom p & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) holds
Sum p = p . i
let p be FinSequence of K; ::_thesis: for i being Nat st i in dom p & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) holds
Sum p = p . i
let i be Nat; ::_thesis: ( i in dom p & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) implies Sum p = p . i )
assume that
A1: i in dom p and
A2: for k being Nat st k in dom p & k <> i holds
p . k = 0. K ; ::_thesis: Sum p = p . i
reconsider a = p . i as Element of K by A1, FINSEQ_2:11;
reconsider p1 = p | (Seg i) as FinSequence of K by FINSEQ_1:18;
 i <> 0 by A1, FINSEQ_3:25;
then  i in Seg i by FINSEQ_1:3;
then  i in (dom p) /\ (Seg i) by A1, XBOOLE_0:def_4;
then A3: i in dom p1 by RELAT_1:61;
then  p1 <> {} ;
then  len p1 <> 0 ;
then consider p3 being FinSequence of K, x being Element of K such that
A4: p1 = p3 ^ <*x*> by FINSEQ_2:19;
 i in NAT by ORDINAL1:def_12;
then  p1 is_a_prefix_of p by TREES_1:def_1;
then consider p2 being FinSequence such that
A5: p = p1 ^ p2 by TREES_1:1;
reconsider p2 = p2 as FinSequence of K by A5, FINSEQ_1:36;
A6: dom p2 = Seg (len p2) by FINSEQ_1:def_3;
A7: for k being Nat st k in Seg (len p2) holds
p2 . k = 0. K
proof
let k be Nat; ::_thesis: ( k in Seg (len p2) implies p2 . k = 0. K )
A8: ( i <= len p1 & len p1 <= (len p1) + k ) by A3, FINSEQ_3:25, NAT_1:12;
assume  k in Seg (len p2) ; ::_thesis: p2 . k = 0. K
then A9: k in dom p2 by FINSEQ_1:def_3;
then  0 <> k by FINSEQ_3:25;
then A10: i <> (len p1) + k by A8, XCMPLX_1:3, XXREAL_0:1;
thus p2 . k = p . ((len p1) + k) by A5, A9, FINSEQ_1:def_7
.= 0. K by A2, A5, A9, A10, FINSEQ_1:28 ; ::_thesis: verum
end;
A11: now__::_thesis:_for_j_being_Nat_st_j_in_dom_p2_holds_
p2_._j_=_((len_p2)_|->_(0._K))_._j
let j be Nat; ::_thesis: ( j in dom p2 implies p2 . j = ((len p2) |-> (0. K)) . j )
assume A12: j in dom p2 ; ::_thesis: p2 . j = ((len p2) |-> (0. K)) . j
hence p2 . j = 0. K by A7, A6
.= ((len p2) |-> (0. K)) . j by A6, A12, FINSEQ_2:57 ;
::_thesis: verum
end;
A13: dom p3 = Seg (len p3) by FINSEQ_1:def_3;
 i <= len p by A1, FINSEQ_3:25;
then A14: i = len p1 by FINSEQ_1:17
.= (len p3) + (len <*x*>) by A4, FINSEQ_1:22
.= (len p3) + 1 by FINSEQ_1:39 ;
then A15: x = p1 . i by A4, FINSEQ_1:42
.= a by A5, A3, FINSEQ_1:def_7 ;
A16: for k being Nat st k in Seg (len p3) holds
p3 . k = 0. K
proof
let k be Nat; ::_thesis: ( k in Seg (len p3) implies p3 . k = 0. K )
assume A17: k in Seg (len p3) ; ::_thesis: p3 . k = 0. K
then  k <= len p3 by FINSEQ_1:1;
then A18: i <> k by A14, NAT_1:13;
A19: k in dom p3 by A17, FINSEQ_1:def_3;
then A20: k in dom p1 by A4, FINSEQ_2:15;
thus p3 . k = p1 . k by A4, A19, FINSEQ_1:def_7
.= p . k by A5, A20, FINSEQ_1:def_7
.= 0. K by A2, A5, A18, A20, FINSEQ_2:15 ; ::_thesis: verum
end;
A21: now__::_thesis:_for_j_being_Nat_st_j_in_dom_p3_holds_
p3_._j_=_((len_p3)_|->_(0._K))_._j
let j be Nat; ::_thesis: ( j in dom p3 implies p3 . j = ((len p3) |-> (0. K)) . j )
assume A22: j in dom p3 ; ::_thesis: p3 . j = ((len p3) |-> (0. K)) . j
hence p3 . j = 0. K by A16, A13
.= ((len p3) |-> (0. K)) . j by A13, A22, FINSEQ_2:57 ;
::_thesis: verum
end;
 len ((len p3) |-> (0. K)) = len p3 by CARD_1:def_7;
then A23: p3 = (len p3) |-> (0. K) by A21, FINSEQ_2:9;
 len ((len p2) |-> (0. K)) = len p2 by CARD_1:def_7;
then  p2 = (len p2) |-> (0. K) by A11, FINSEQ_2:9;
then  Sum p = (Sum (p3 ^ <*x*>)) + (Sum ((len p2) |-> (0. K))) by A5, A4, RLVECT_1:41
.= (Sum (p3 ^ <*x*>)) + (0. K) by Th11
.= Sum (p3 ^ <*x*>) by RLVECT_1:4
.= (Sum ((len p3) |-> (0. K))) + x by A23, FVSUM_1:71
.= (0. K) + a by A15, Th11
.= p . i by RLVECT_1:4 ;
hence  Sum p = p . i ; ::_thesis: verum
end;

theorem Th13: :: MATRIX_3:13
for K being Field
for p, q being FinSequence of K holds len (mlt (p,q)) = min ((len p),(len q))
proof
let K be Field; ::_thesis: for p, q being FinSequence of K holds len (mlt (p,q)) = min ((len p),(len q))
let p, q be FinSequence of K; ::_thesis: len (mlt (p,q)) = min ((len p),(len q))
reconsider r = mlt (p,q) as FinSequence of K ;
 r = the multF of K .: (p,q) by FVSUM_1:def_7;
hence  len (mlt (p,q)) = min ((len p),(len q)) by FINSEQ_2:71; ::_thesis: verum
end;

theorem Th14: :: MATRIX_3:14
for K being Field
for p, q being FinSequence of K
for i being Nat st p . i = 1. K & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) holds
for j being Nat st j in dom (mlt (p,q)) holds
( ( i = j implies (mlt (p,q)) . j = q . i ) & ( i <> j implies (mlt (p,q)) . j = 0. K ) )
proof
let K be Field; ::_thesis: for p, q being FinSequence of K
for i being Nat st p . i = 1. K & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) holds
for j being Nat st j in dom (mlt (p,q)) holds
( ( i = j implies (mlt (p,q)) . j = q . i ) & ( i <> j implies (mlt (p,q)) . j = 0. K ) )
let p, q be FinSequence of K; ::_thesis: for i being Nat st p . i = 1. K & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) holds
for j being Nat st j in dom (mlt (p,q)) holds
( ( i = j implies (mlt (p,q)) . j = q . i ) & ( i <> j implies (mlt (p,q)) . j = 0. K ) )
let i be Nat; ::_thesis: ( p . i = 1. K & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) implies for j being Nat st j in dom (mlt (p,q)) holds
( ( i = j implies (mlt (p,q)) . j = q . i ) & ( i <> j implies (mlt (p,q)) . j = 0. K ) ) )
assume that
A1: p . i = 1. K and
A2: for k being Nat st k in dom p & k <> i holds
p . k = 0. K ; ::_thesis: for j being Nat st j in dom (mlt (p,q)) holds
( ( i = j implies (mlt (p,q)) . j = q . i ) & ( i <> j implies (mlt (p,q)) . j = 0. K ) )
let j be Nat; ::_thesis: ( j in dom (mlt (p,q)) implies ( ( i = j implies (mlt (p,q)) . j = q . i ) & ( i <> j implies (mlt (p,q)) . j = 0. K ) ) )
assume A3: j in dom (mlt (p,q)) ; ::_thesis: ( ( i = j implies (mlt (p,q)) . j = q . i ) & ( i <> j implies (mlt (p,q)) . j = 0. K ) )
A4: ( dom p = Seg (len p) & dom q = Seg (len q) ) by FINSEQ_1:def_3;
reconsider j1 = j as Element of NAT by ORDINAL1:def_12;
 ( dom (mlt (p,q)) = Seg (len (mlt (p,q))) & len (mlt (p,q)) = min ((len p),(len q)) ) by Th13, FINSEQ_1:def_3;
then A5: j in (dom p) /\ (dom q) by A3, A4, FINSEQ_2:2;
then A6: j in dom q by XBOOLE_0:def_4;
then reconsider b = q . j1 as Element of K by FINSEQ_2:11;
thus  ( i = j implies (mlt (p,q)) . j = q . i ) ::_thesis: ( i <> j implies (mlt (p,q)) . j = 0. K )
proof
reconsider b = q . j1 as Element of K by A6, FINSEQ_2:11;
assume A7: i = j ; ::_thesis: (mlt (p,q)) . j = q . i
hence (mlt (p,q)) . j = b * (1. K) by A1, A3, FVSUM_1:60
.= q . i by A7, VECTSP_1:def_8 ;
::_thesis: verum
end;
assume A8: i <> j ; ::_thesis: (mlt (p,q)) . j = 0. K
 j in dom p by A5, XBOOLE_0:def_4;
then  p . j = 0. K by A2, A8;
hence (mlt (p,q)) . j = (0. K) * b by A3, FVSUM_1:60
.= 0. K by VECTSP_1:12 ;
::_thesis: verum
end;

theorem Th15: :: MATRIX_3:15
for n being Nat
for K being Field
for i, j being Nat st [i,j] in Indices (1. (K,n)) holds
( ( i = j implies (Line ((1. (K,n)),i)) . j = 1. K ) & ( i <> j implies (Line ((1. (K,n)),i)) . j = 0. K ) )
proof
let n be Nat; ::_thesis: for K being Field
for i, j being Nat st [i,j] in Indices (1. (K,n)) holds
( ( i = j implies (Line ((1. (K,n)),i)) . j = 1. K ) & ( i <> j implies (Line ((1. (K,n)),i)) . j = 0. K ) )
let K be Field; ::_thesis: for i, j being Nat st [i,j] in Indices (1. (K,n)) holds
( ( i = j implies (Line ((1. (K,n)),i)) . j = 1. K ) & ( i <> j implies (Line ((1. (K,n)),i)) . j = 0. K ) )
let i, j be Nat; ::_thesis: ( [i,j] in Indices (1. (K,n)) implies ( ( i = j implies (Line ((1. (K,n)),i)) . j = 1. K ) & ( i <> j implies (Line ((1. (K,n)),i)) . j = 0. K ) ) )
set B = 1. (K,n);
assume A1: [i,j] in Indices (1. (K,n)) ; ::_thesis: ( ( i = j implies (Line ((1. (K,n)),i)) . j = 1. K ) & ( i <> j implies (Line ((1. (K,n)),i)) . j = 0. K ) )
then  j in Seg (width (1. (K,n))) by ZFMISC_1:87;
then A2: (Line ((1. (K,n)),i)) . j = (1. (K,n)) * (i,j) by MATRIX_1:def_7;
hence  ( i = j implies (Line ((1. (K,n)),i)) . j = 1. K ) by A1, MATRIX_1:def_11; ::_thesis: ( i <> j implies (Line ((1. (K,n)),i)) . j = 0. K )
thus  ( i <> j implies (Line ((1. (K,n)),i)) . j = 0. K ) by A1, A2, MATRIX_1:def_11; ::_thesis: verum
end;

theorem Th16: :: MATRIX_3:16
for n being Nat
for K being Field
for i, j being Nat st [i,j] in Indices (1. (K,n)) holds
( ( i = j implies (Col ((1. (K,n)),j)) . i = 1. K ) & ( i <> j implies (Col ((1. (K,n)),j)) . i = 0. K ) )
proof
let n be Nat; ::_thesis: for K being Field
for i, j being Nat st [i,j] in Indices (1. (K,n)) holds
( ( i = j implies (Col ((1. (K,n)),j)) . i = 1. K ) & ( i <> j implies (Col ((1. (K,n)),j)) . i = 0. K ) )
let K be Field; ::_thesis: for i, j being Nat st [i,j] in Indices (1. (K,n)) holds
( ( i = j implies (Col ((1. (K,n)),j)) . i = 1. K ) & ( i <> j implies (Col ((1. (K,n)),j)) . i = 0. K ) )
let i, j be Nat; ::_thesis: ( [i,j] in Indices (1. (K,n)) implies ( ( i = j implies (Col ((1. (K,n)),j)) . i = 1. K ) & ( i <> j implies (Col ((1. (K,n)),j)) . i = 0. K ) ) )
set B = 1. (K,n);
assume A1: [i,j] in Indices (1. (K,n)) ; ::_thesis: ( ( i = j implies (Col ((1. (K,n)),j)) . i = 1. K ) & ( i <> j implies (Col ((1. (K,n)),j)) . i = 0. K ) )
then  i in dom (1. (K,n)) by ZFMISC_1:87;
then A2: (Col ((1. (K,n)),j)) . i = (1. (K,n)) * (i,j) by MATRIX_1:def_8;
hence  ( i = j implies (Col ((1. (K,n)),j)) . i = 1. K ) by A1, MATRIX_1:def_11; ::_thesis: ( i <> j implies (Col ((1. (K,n)),j)) . i = 0. K )
thus  ( i <> j implies (Col ((1. (K,n)),j)) . i = 0. K ) by A1, A2, MATRIX_1:def_11; ::_thesis: verum
end;

theorem Th17: :: MATRIX_3:17
for K being Field
for p, q being FinSequence of K
for i being Nat st i in dom p & i in dom q & p . i = 1. K & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) holds
Sum (mlt (p,q)) = q . i
proof
let K be Field; ::_thesis: for p, q being FinSequence of K
for i being Nat st i in dom p & i in dom q & p . i = 1. K & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) holds
Sum (mlt (p,q)) = q . i
let p, q be FinSequence of K; ::_thesis: for i being Nat st i in dom p & i in dom q & p . i = 1. K & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) holds
Sum (mlt (p,q)) = q . i
let i be Nat; ::_thesis: ( i in dom p & i in dom q & p . i = 1. K & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) implies Sum (mlt (p,q)) = q . i )
assume that
A1: ( i in dom p & i in dom q ) and
A2: ( p . i = 1. K & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) ) ; ::_thesis: Sum (mlt (p,q)) = q . i
reconsider r = mlt (p,q) as FinSequence of K ;
A3: for k being Nat st k in dom r & k <> i holds
r . k = 0. K by A2, Th14;
A4: ( dom p = Seg (len p) & dom q = Seg (len q) ) by FINSEQ_1:def_3;
 ( dom (mlt (p,q)) = Seg (len (mlt (p,q))) & len (mlt (p,q)) = min ((len p),(len q)) ) by Th13, FINSEQ_1:def_3;
then  (dom p) /\ (dom q) = dom (mlt (p,q)) by A4, FINSEQ_2:2;
then A5: i in dom r by A1, XBOOLE_0:def_4;
then  r . i = q . i by A2, Th14;
hence  Sum (mlt (p,q)) = q . i by A5, A3, Th12; ::_thesis: verum
end;

theorem :: MATRIX_3:18
for n being Nat
for K being Field
for A being Matrix of n,K holds (1. (K,n)) * A = A
proof
let n be Nat; ::_thesis: for K being Field
for A being Matrix of n,K holds (1. (K,n)) * A = A
let K be Field; ::_thesis: for A being Matrix of n,K holds (1. (K,n)) * A = A
let A be Matrix of n,K; ::_thesis: (1. (K,n)) * A = A
set B = 1. (K,n);
A1: len (1. (K,n)) = n by MATRIX_1:24;
A2: len A = n by MATRIX_1:24;
A3: width (1. (K,n)) = n by MATRIX_1:24;
then A4: len ((1. (K,n)) * A) = len (1. (K,n)) by A2, Def4;
A5: now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_((1._(K,n))_*_A)_holds_
((1._(K,n))_*_A)_*_(i,j)_=_A_*_(i,j)
A6: dom A = Seg (len A) by FINSEQ_1:def_3;
let i, j be Nat; ::_thesis: ( [i,j] in Indices ((1. (K,n)) * A) implies ((1. (K,n)) * A) * (i,j) = A * (i,j) )
assume A7: [i,j] in Indices ((1. (K,n)) * A) ; ::_thesis: ((1. (K,n)) * A) * (i,j) = A * (i,j)
A8: ( dom ((1. (K,n)) * A) = Seg (len ((1. (K,n)) * A)) & Indices ((1. (K,n)) * A) = [:(dom ((1. (K,n)) * A)),(Seg (width ((1. (K,n)) * A))):] ) by FINSEQ_1:def_3;
then A9: i in Seg (width (1. (K,n))) by A1, A3, A4, A7, ZFMISC_1:87;
then  i in Seg (len (Line ((1. (K,n)),i))) by MATRIX_1:def_7;
then A10: i in dom (Line ((1. (K,n)),i)) by FINSEQ_1:def_3;
A11: dom (1. (K,n)) = Seg (len (1. (K,n))) by FINSEQ_1:def_3;
then A12: i in dom (1. (K,n)) by A4, A7, A8, ZFMISC_1:87;
then  [i,i] in [:(dom (1. (K,n))),(Seg (width (1. (K,n)))):] by A9, ZFMISC_1:87;
then  [i,i] in Indices (1. (K,n)) ;
then A13: (Line ((1. (K,n)),i)) . i = 1. K by Th15;
A14: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(Line_((1._(K,n)),i))_&_k_<>_i_holds_
(Line_((1._(K,n)),i))_._k_=_0._K
let k be Nat; ::_thesis: ( k in dom (Line ((1. (K,n)),i)) & k <> i implies (Line ((1. (K,n)),i)) . k = 0. K )
assume that
A15: k in dom (Line ((1. (K,n)),i)) and
A16: k <> i ; ::_thesis: (Line ((1. (K,n)),i)) . k = 0. K
 k in Seg (len (Line ((1. (K,n)),i))) by A15, FINSEQ_1:def_3;
then  k in Seg (width (1. (K,n))) by MATRIX_1:def_7;
then  [i,k] in [:(dom (1. (K,n))),(Seg (width (1. (K,n)))):] by A12, ZFMISC_1:87;
then  [i,k] in Indices (1. (K,n)) ;
hence  (Line ((1. (K,n)),i)) . k = 0. K by A16, Th15; ::_thesis: verum
end;
 i in Seg (len (Col (A,j))) by A3, A2, A9, MATRIX_1:def_8;
then A17: i in dom (Col (A,j)) by FINSEQ_1:def_3;
thus ((1. (K,n)) * A) * (i,j) = (Line ((1. (K,n)),i)) "*" (Col (A,j)) by A3, A2, A7, Def4
.= Sum (mlt ((Line ((1. (K,n)),i)),(Col (A,j)))) by FVSUM_1:def_9
.= (Col (A,j)) . i by A10, A17, A14, A13, Th17
.= A * (i,j) by A1, A2, A6, A11, A12, MATRIX_1:def_8 ; ::_thesis: verum
end;
 width ((1. (K,n)) * A) = width A by A3, A2, Def4;
hence  (1. (K,n)) * A = A by A1, A2, A4, A5, MATRIX_1:21; ::_thesis: verum
end;

theorem :: MATRIX_3:19
for n being Nat
for K being Field
for A being Matrix of n,K holds A * (1. (K,n)) = A
proof
let n be Nat; ::_thesis: for K being Field
for A being Matrix of n,K holds A * (1. (K,n)) = A
let K be Field; ::_thesis: for A being Matrix of n,K holds A * (1. (K,n)) = A
let A be Matrix of n,K; ::_thesis: A * (1. (K,n)) = A
set B = 1. (K,n);
A1: width (1. (K,n)) = n by MATRIX_1:24;
A2: width A = n by MATRIX_1:24;
A3: len (1. (K,n)) = n by MATRIX_1:24;
then A4: width (A * (1. (K,n))) = width (1. (K,n)) by A2, Def4;
A5: now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_(A_*_(1._(K,n)))_holds_
(A_*_(1._(K,n)))_*_(i,j)_=_A_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices (A * (1. (K,n))) implies (A * (1. (K,n))) * (i,j) = A * (i,j) )
assume A6: [i,j] in Indices (A * (1. (K,n))) ; ::_thesis: (A * (1. (K,n))) * (i,j) = A * (i,j)
then A7: j in Seg (width (1. (K,n))) by A4, ZFMISC_1:87;
then  j in Seg (len (Col ((1. (K,n)),j))) by A3, A1, MATRIX_1:def_8;
then A8: j in dom (Col ((1. (K,n)),j)) by FINSEQ_1:def_3;
A9: j in Seg (width A) by A1, A2, A4, A6, ZFMISC_1:87;
A10: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(Col_((1._(K,n)),j))_&_k_<>_j_holds_
(Col_((1._(K,n)),j))_._k_=_0._K
let k be Nat; ::_thesis: ( k in dom (Col ((1. (K,n)),j)) & k <> j implies (Col ((1. (K,n)),j)) . k = 0. K )
assume that
A11: k in dom (Col ((1. (K,n)),j)) and
A12: k <> j ; ::_thesis: (Col ((1. (K,n)),j)) . k = 0. K
 k in Seg (len (Col ((1. (K,n)),j))) by A11, FINSEQ_1:def_3;
then  k in Seg (len (1. (K,n))) by MATRIX_1:def_8;
then  k in dom (1. (K,n)) by FINSEQ_1:def_3;
then  [k,j] in [:(dom (1. (K,n))),(Seg (width (1. (K,n)))):] by A7, ZFMISC_1:87;
then  [k,j] in Indices (1. (K,n)) ;
hence  (Col ((1. (K,n)),j)) . k = 0. K by A12, Th16; ::_thesis: verum
end;
 j in dom (1. (K,n)) by A3, A1, A7, FINSEQ_1:def_3;
then  [j,j] in [:(dom (1. (K,n))),(Seg (width (1. (K,n)))):] by A1, A2, A9, ZFMISC_1:87;
then  [j,j] in Indices (1. (K,n)) ;
then A13: (Col ((1. (K,n)),j)) . j = 1. K by Th16;
 j in Seg (len (Line (A,i))) by A1, A2, A7, MATRIX_1:def_7;
then A14: j in dom (Line (A,i)) by FINSEQ_1:def_3;
thus (A * (1. (K,n))) * (i,j) = (Line (A,i)) "*" (Col ((1. (K,n)),j)) by A3, A2, A6, Def4
.= (Col ((1. (K,n)),j)) "*" (Line (A,i)) by FVSUM_1:90
.= Sum (mlt ((Col ((1. (K,n)),j)),(Line (A,i)))) by FVSUM_1:def_9
.= (Line (A,i)) . j by A8, A14, A10, A13, Th17
.= A * (i,j) by A9, MATRIX_1:def_7 ; ::_thesis: verum
end;
 len (A * (1. (K,n))) = len A by A3, A2, Def4;
hence  A * (1. (K,n)) = A by A1, A2, A4, A5, MATRIX_1:21; ::_thesis: verum
end;

theorem :: MATRIX_3:20
for K being Field
for a, b being Element of K holds <*<*a*>*> * <*<*b*>*> = <*<*(a * b)*>*>
proof
let K be Field; ::_thesis: for a, b being Element of K holds <*<*a*>*> * <*<*b*>*> = <*<*(a * b)*>*>
let a, b be Element of K; ::_thesis: <*<*a*>*> * <*<*b*>*> = <*<*(a * b)*>*>
reconsider A = <*<*a*>*> as Matrix of 1,K ;
reconsider B = <*<*b*>*> as Matrix of 1,K ;
reconsider C = A * B as Matrix of K ;
A1: len (Line (A,1)) = width A by MATRIX_1:def_7
.= 1 by MATRIX_1:24 ;
A2: width A = 1 by MATRIX_1:24;
then  1 in Seg (width A) by FINSEQ_1:2, TARSKI:def_1;
then (Line (A,1)) . 1 = <*<*a*>*> * (1,1) by MATRIX_1:def_7
.= a by MATRIX_2:5 ;
then A3: Line (<*<*a*>*>,1) = <*a*> by A1, FINSEQ_1:40;
A4: len B = 1 by MATRIX_1:24;
then  1 in Seg (len B) by FINSEQ_1:2, TARSKI:def_1;
then  1 in dom B by FINSEQ_1:def_3;
then A5: (Col (B,1)) . 1 = <*<*b*>*> * (1,1) by MATRIX_1:def_8
.= b by MATRIX_2:5 ;
 len A = 1 by MATRIX_1:24;
then A6: len C = 1 by A2, A4, Def4;
 width B = 1 by MATRIX_1:24;
then A7: width C = 1 by A2, A4, Def4;
then reconsider C = C as Matrix of 1,K by A6, MATRIX_2:7;
 Seg (len C) = dom C by FINSEQ_1:def_3;
then A8: Indices C = [:(Seg 1),(Seg 1):] by A6, A7;
len (Col (B,1)) = len B by MATRIX_1:def_8
.= 1 by MATRIX_1:24 ;
then A9: Col (<*<*b*>*>,1) = <*b*> by A5, FINSEQ_1:40;
now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_C_holds_
C_*_(i,j)_=_<*<*(a_*_b)*>*>_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices C implies C * (i,j) = <*<*(a * b)*>*> * (i,j) )
assume A10: [i,j] in Indices C ; ::_thesis: C * (i,j) = <*<*(a * b)*>*> * (i,j)
then  j in Seg 1 by A8, ZFMISC_1:87;
then A11: j = 1 by FINSEQ_1:2, TARSKI:def_1;
 i in Seg 1 by A8, A10, ZFMISC_1:87;
then A12: i = 1 by FINSEQ_1:2, TARSKI:def_1;
hence C * (i,j) = <*a*> "*" <*b*> by A2, A4, A3, A9, A10, A11, Def4
.= a * b by FVSUM_1:88
.= <*<*(a * b)*>*> * (i,j) by A12, A11, MATRIX_2:5 ;
::_thesis: verum
end;
hence  <*<*a*>*> * <*<*b*>*> = <*<*(a * b)*>*> by MATRIX_1:27; ::_thesis: verum
end;

theorem :: MATRIX_3:21
for K being Field
for a1, a2, b1, b2, c1, c2, d1, d2 being Element of K holds ((a1,b1) ][ (c1,d1)) * ((a2,b2) ][ (c2,d2)) = (((a1 * a2) + (b1 * c2)),((a1 * b2) + (b1 * d2))) ][ (((c1 * a2) + (d1 * c2)),((c1 * b2) + (d1 * d2)))
proof
let K be Field; ::_thesis: for a1, a2, b1, b2, c1, c2, d1, d2 being Element of K holds ((a1,b1) ][ (c1,d1)) * ((a2,b2) ][ (c2,d2)) = (((a1 * a2) + (b1 * c2)),((a1 * b2) + (b1 * d2))) ][ (((c1 * a2) + (d1 * c2)),((c1 * b2) + (d1 * d2)))
let a1, a2, b1, b2, c1, c2, d1, d2 be Element of K; ::_thesis: ((a1,b1) ][ (c1,d1)) * ((a2,b2) ][ (c2,d2)) = (((a1 * a2) + (b1 * c2)),((a1 * b2) + (b1 * d2))) ][ (((c1 * a2) + (d1 * c2)),((c1 * b2) + (d1 * d2)))
reconsider A = (a1,b1) ][ (c1,d1) as Matrix of 2,K ;
reconsider B = (a2,b2) ][ (c2,d2) as Matrix of 2,K ;
reconsider D = (((a1 * a2) + (b1 * c2)),((a1 * b2) + (b1 * d2))) ][ (((c1 * a2) + (d1 * c2)),((c1 * b2) + (d1 * d2))) as Matrix of 2,K ;
A1: width A = 2 by MATRIX_1:24;
 2 in {1,2} by TARSKI:def_2;
then A2: (Line (A,2)) . 2 = A * (2,2) by A1, FINSEQ_1:2, MATRIX_1:def_7
.= d1 by MATRIX_2:6 ;
A3: len (Line (A,2)) = width A by MATRIX_1:def_7
.= 2 by MATRIX_1:24 ;
 1 in {1,2} by TARSKI:def_2;
then (Line (A,2)) . 1 = A * (2,1) by A1, FINSEQ_1:2, MATRIX_1:def_7
.= c1 by MATRIX_2:6 ;
then A4: Line (A,2) = <*c1,d1*> by A3, A2, FINSEQ_1:44;
 2 in {1,2} by TARSKI:def_2;
then A5: (Line (A,1)) . 2 = A * (1,2) by A1, FINSEQ_1:2, MATRIX_1:def_7
.= b1 by MATRIX_2:6 ;
A6: len (Line (A,1)) = width A by MATRIX_1:def_7
.= 2 by MATRIX_1:24 ;
 1 in {1,2} by TARSKI:def_2;
then (Line (A,1)) . 1 = A * (1,1) by A1, FINSEQ_1:2, MATRIX_1:def_7
.= a1 by MATRIX_2:6 ;
then A7: Line (A,1) = <*a1,b1*> by A6, A5, FINSEQ_1:44;
A8: len (Col (B,2)) = len B by MATRIX_1:def_8
.= 2 by MATRIX_1:24 ;
A9: len (Col (B,1)) = len B by MATRIX_1:def_8
.= 2 by MATRIX_1:24 ;
reconsider C = A * B as Matrix of K ;
A10: len B = 2 by MATRIX_1:24;
 width B = 2 by MATRIX_1:24;
then A11: width C = 2 by A1, A10, Def4;
 len A = 2 by MATRIX_1:24;
then A12: len C = 2 by A1, A10, Def4;
then reconsider C = C as Matrix of 2,K by A11, MATRIX_2:7;
A13: Seg (len B) = dom B by FINSEQ_1:def_3;
 2 in {1,2} by TARSKI:def_2;
then A14: (Col (B,2)) . 2 = B * (2,2) by A10, A13, FINSEQ_1:2, MATRIX_1:def_8
.= d2 by MATRIX_2:6 ;
 1 in {1,2} by TARSKI:def_2;
then (Col (B,2)) . 1 = B * (1,2) by A10, A13, FINSEQ_1:2, MATRIX_1:def_8
.= b2 by MATRIX_2:6 ;
then A15: Col (B,2) = <*b2,d2*> by A8, A14, FINSEQ_1:44;
 2 in {1,2} by TARSKI:def_2;
then A16: (Col (B,1)) . 2 = B * (2,1) by A10, A13, FINSEQ_1:2, MATRIX_1:def_8
.= c2 by MATRIX_2:6 ;
 1 in {1,2} by TARSKI:def_2;
then (Col (B,1)) . 1 = B * (1,1) by A10, A13, FINSEQ_1:2, MATRIX_1:def_8
.= a2 by MATRIX_2:6 ;
then A17: Col (B,1) = <*a2,c2*> by A9, A16, FINSEQ_1:44;
 dom C = Seg (len C) by FINSEQ_1:def_3;
then A18: Indices C = [:(Seg 2),(Seg 2):] by A12, A11;
now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_C_holds_
C_*_(i,j)_=_D_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices C implies C * (i,j) = D * (i,j) )
assume A19: [i,j] in Indices C ; ::_thesis: C * (i,j) = D * (i,j)
then A20: ( i in Seg 2 & j in Seg 2 ) by A18, ZFMISC_1:87;
now__::_thesis:_(_(_i_=_1_&_j_=_1_&_C_*_(1,1)_=_D_*_(1,1)_)_or_(_i_=_1_&_j_=_2_&_C_*_(1,2)_=_D_*_(1,2)_)_or_(_i_=_2_&_j_=_1_&_C_*_(2,1)_=_D_*_(2,1)_)_or_(_i_=_2_&_j_=_2_&_C_*_(2,2)_=_D_*_(2,2)_)_)
percases ( ( i = 1 & j = 1 ) or ( i = 1 & j = 2 ) or ( i = 2 & j = 1 ) or ( i = 2 & j = 2 ) ) by A20, FINSEQ_1:2, TARSKI:def_2;
case ( i = 1 & j = 1 ) ; ::_thesis: C * (1,1) = D * (1,1)
hence C * (1,1) = <*a1,b1*> "*" <*a2,c2*> by A1, A10, A7, A17, A19, Def4
.= (a1 * a2) + (b1 * c2) by FVSUM_1:89
.= D * (1,1) by MATRIX_2:6 ;
::_thesis: verum
end;
case ( i = 1 & j = 2 ) ; ::_thesis: C * (1,2) = D * (1,2)
hence C * (1,2) = <*a1,b1*> "*" <*b2,d2*> by A1, A10, A7, A15, A19, Def4
.= (a1 * b2) + (b1 * d2) by FVSUM_1:89
.= D * (1,2) by MATRIX_2:6 ;
::_thesis: verum
end;
case ( i = 2 & j = 1 ) ; ::_thesis: C * (2,1) = D * (2,1)
hence C * (2,1) = <*c1,d1*> "*" <*a2,c2*> by A1, A10, A4, A17, A19, Def4
.= (c1 * a2) + (d1 * c2) by FVSUM_1:89
.= D * (2,1) by MATRIX_2:6 ;
::_thesis: verum
end;
case ( i = 2 & j = 2 ) ; ::_thesis: C * (2,2) = D * (2,2)
hence C * (2,2) = <*c1,d1*> "*" <*b2,d2*> by A1, A10, A4, A15, A19, Def4
.= (c1 * b2) + (d1 * d2) by FVSUM_1:89
.= D * (2,2) by MATRIX_2:6 ;
::_thesis: verum
end;
end;
end;
hence  C * (i,j) = D * (i,j) ; ::_thesis: verum
end;
hence  ((a1,b1) ][ (c1,d1)) * ((a2,b2) ][ (c2,d2)) = (((a1 * a2) + (b1 * c2)),((a1 * b2) + (b1 * d2))) ][ (((c1 * a2) + (d1 * c2)),((c1 * b2) + (d1 * d2))) by MATRIX_1:27; ::_thesis: verum
end;

theorem :: MATRIX_3:22
for K being Field
for A, B being Matrix of K st width A = len B & width B <> 0 holds
(A * B) @ = (B @) * (A @)
proof
let K be Field; ::_thesis: for A, B being Matrix of K st width A = len B & width B <> 0 holds
(A * B) @ = (B @) * (A @)
let A, B be Matrix of K; ::_thesis: ( width A = len B & width B <> 0 implies (A * B) @ = (B @) * (A @) )
assume that
A1: width A = len B and
A2: width B <> 0 ; ::_thesis: (A * B) @ = (B @) * (A @)
A3: len (B @) = width B by MATRIX_1:def_6;
 len (A @) = width A by MATRIX_1:def_6;
then A4: width (B @) = len (A @) by A1, A2, MATRIX_2:10;
then A5: width ((B @) * (A @)) = width (A @) by Def4;
 width (A * B) > 0 by A1, A2, Def4;
then A6: width ((A * B) @) = len (A * B) by MATRIX_2:10
.= len A by A1, Def4 ;
A7: width ((B @) * (A @)) = width (A @) by A4, Def4;
A8: len ((B @) * (A @)) = len (B @) by A4, Def4
.= width B by MATRIX_1:def_6 ;
A9: len ((B @) * (A @)) = len (B @) by A4, Def4;
A10: now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_((B_@)_*_(A_@))_holds_
((B_@)_*_(A_@))_*_(i,j)_=_((A_*_B)_@)_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices ((B @) * (A @)) implies ((B @) * (A @)) * (b1,b2) = ((A * B) @) * (b1,b2) )
assume A11: [i,j] in Indices ((B @) * (A @)) ; ::_thesis: ((B @) * (A @)) * (b1,b2) = ((A * B) @) * (b1,b2)
 dom ((B @) * (A @)) = dom (B @) by A9, FINSEQ_3:29;
then A12: [i,j] in [:(dom (B @)),(Seg (width (A @))):] by A5, A11;
percases ( width A = 0 or width A > 0 ) ;
suppose width A = 0 ; ::_thesis: ((B @) * (A @)) * (b1,b2) = ((A * B) @) * (b1,b2)
hence  ((B @) * (A @)) * (i,j) = ((A * B) @) * (i,j) by A1, A2, MATRIX_1:def_3; ::_thesis: verum
end;
suppose width A > 0 ; ::_thesis: ((B @) * (A @)) * (b1,b2) = ((A * B) @) * (b1,b2)
then  width (A @) = len A by MATRIX_2:10;
then  Seg (width (A @)) = dom A by FINSEQ_1:def_3;
then A13: j in dom A by A12, ZFMISC_1:87;
then A14: Col ((A @),j) = Line (A,j) by MATRIX_2:14;
 j in Seg (len A) by A13, FINSEQ_1:def_3;
then  j in Seg (len (A * B)) by A1, Def4;
then A15: j in dom (A * B) by FINSEQ_1:def_3;
 Seg (width B) = dom (B @) by A3, FINSEQ_1:def_3;
then A16: i in Seg (width B) by A12, ZFMISC_1:87;
then  i in Seg (width (A * B)) by A1, Def4;
then  [j,i] in [:(dom (A * B)),(Seg (width (A * B))):] by A15, ZFMISC_1:87;
then A17: [j,i] in Indices (A * B) ;
 Line ((B @),i) = Col (B,i) by A16, MATRIX_2:15;
hence ((B @) * (A @)) * (i,j) = (Col (B,i)) "*" (Line (A,j)) by A4, A11, A14, Def4
.= (Line (A,j)) "*" (Col (B,i)) by FVSUM_1:90
.= (A * B) * (j,i) by A1, A17, Def4
.= ((A * B) @) * (i,j) by A17, MATRIX_1:def_6 ;
::_thesis: verum
end;
end;
end;
A18: width (A @) = len A
proof
percases ( width A = 0 or width A > 0 ) ;
suppose width A = 0 ; ::_thesis: width (A @) = len A
hence  width (A @) = len A by A1, A2, MATRIX_1:def_3; ::_thesis: verum
end;
suppose width A > 0 ; ::_thesis: width (A @) = len A
hence  width (A @) = len A by MATRIX_2:10; ::_thesis: verum
end;
end;
end;
len ((A * B) @) = width (A * B) by MATRIX_1:def_6
.= width B by A1, Def4 ;
hence  (A * B) @ = (B @) * (A @) by A6, A8, A7, A10, A18, MATRIX_1:21; ::_thesis: verum
end;

begin

definition
let I, J be non empty set ;
let X be Element of Fin I;
let Y be Element of Fin J;
:: original: [:
redefine func[:X,Y:] ->  Element of Fin [:I,J:];
coherence
 [:X,Y:] is Element of Fin [:I,J:]
proof
 ( X c= I & Y c= J ) by FINSUB_1:def_5;
then  [:X,Y:] c= [:I,J:] by ZFMISC_1:96;
hence  [:X,Y:] is Element of Fin [:I,J:] by FINSUB_1:def_5; ::_thesis: verum
end;
end;

definition
let I, J, D be non empty set ;
let G be BinOp of D;
let f be Function of I,D;
let g be Function of J,D;
:: original: *
redefine funcG * (f,g) ->  Function of [:I,J:],D;
coherence
 G * (f,g) is Function of [:I,J:],D by FINSEQOP:79;
end;

theorem Th23: :: MATRIX_3:23
for I, J, D being non empty set
for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f)))
proof
deffunc H1( set , set ) ->  set = [$2,$1];
let I, J, D be non empty set ; ::_thesis: for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f)))
let F, G be BinOp of D; ::_thesis: for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f)))
let f be Function of I,D; ::_thesis: for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f)))
let g be Function of J,D; ::_thesis: for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f)))
let X be Element of Fin I; ::_thesis: for Y being Element of Fin J st F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f)))
let Y be Element of Fin J; ::_thesis: ( F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative implies F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f))) )
assume A1: ( F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) ) ; ::_thesis: ( not G is commutative or F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f))) )
consider h being Function such that
A2: ( dom h = [:J,I:] & ( for x, y being set st x in J & y in I holds
h . (x,y) = H1(x,y) ) ) from FUNCT_3:sch_2();
now__::_thesis:_for_z1,_z2_being_set_st_z1_in_dom_h_&_z2_in_dom_h_&_h_._z1_=_h_._z2_holds_
z1_=_z2
let z1, z2 be set ; ::_thesis: ( z1 in dom h & z2 in dom h & h . z1 = h . z2 implies z1 = z2 )
assume that
A3: z1 in dom h and
A4: z2 in dom h and
A5: h . z1 = h . z2 ; ::_thesis: z1 = z2
consider x2, y2 being set  such that
A6: z2 = [x2,y2] by A2, A4, RELAT_1:def_1;
 ( x2 in J & y2 in I ) by A2, A4, A6, ZFMISC_1:87;
then A7: h . (x2,y2) = [y2,x2] by A2;
consider x1, y1 being set  such that
A8: z1 = [x1,y1] by A2, A3, RELAT_1:def_1;
 ( x1 in J & y1 in I ) by A2, A3, A8, ZFMISC_1:87;
then A9: h . (x1,y1) = [y1,x1] by A2;
then  y1 = y2 by A5, A8, A6, A7, XTUPLE_0:1;
hence  z1 = z2 by A5, A8, A6, A9, A7, XTUPLE_0:1; ::_thesis: verum
end;
then A10: h is one-to-one by FUNCT_1:def_4;
A11: for x being set st x in [:J,I:] holds
h . x in [:I,J:]
proof
let x be set ; ::_thesis: ( x in [:J,I:] implies h . x in [:I,J:] )
assume A12: x in [:J,I:] ; ::_thesis: h . x in [:I,J:]
then consider y, z being set  such that
A13: x = [y,z] by RELAT_1:def_1;
A14: ( y in J & z in I ) by A12, A13, ZFMISC_1:87;
then  h . (y,z) = [z,y] by A2;
hence  h . x in [:I,J:] by A13, A14, ZFMISC_1:87; ::_thesis: verum
end;
assume A15: G is commutative ; ::_thesis: F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f)))
A16: G * (g,f) = (G * (f,g)) * h
proof
reconsider G = G as Function of [:D,D:],D ;
A17: dom (G * (g,f)) = [:J,I:] by FUNCT_2:def_1;
A18: dom (G * (f,g)) = [:I,J:] by FUNCT_2:def_1;
A19: for x being set holds
( x in dom (G * (g,f)) iff ( x in dom h & h . x in dom (G * (f,g)) ) )
proof
let x be set ; ::_thesis: ( x in dom (G * (g,f)) iff ( x in dom h & h . x in dom (G * (f,g)) ) )
thus  ( x in dom (G * (g,f)) implies ( x in dom h & h . x in dom (G * (f,g)) ) ) ::_thesis: ( x in dom h & h . x in dom (G * (f,g)) implies x in dom (G * (g,f)) )
proof
assume A20: x in dom (G * (g,f)) ; ::_thesis: ( x in dom h & h . x in dom (G * (f,g)) )
then consider y, z being set  such that
A21: x = [y,z] by RELAT_1:def_1;
A22: ( y in J & z in I ) by A17, A20, A21, ZFMISC_1:87;
then  h . (y,z) = [z,y] by A2;
hence  ( x in dom h & h . x in dom (G * (f,g)) ) by A2, A18, A21, A22, ZFMISC_1:87; ::_thesis: verum
end;
assume that
A23: x in dom h and
 h . x in dom (G * (f,g)) ; ::_thesis: x in dom (G * (g,f))
thus  x in dom (G * (g,f)) by A2, A23, FUNCT_2:def_1; ::_thesis: verum
end;
 for x being set st x in dom (G * (g,f)) holds
(G * (g,f)) . x = (G * (f,g)) . (h . x)
proof
let x be set ; ::_thesis: ( x in dom (G * (g,f)) implies (G * (g,f)) . x = (G * (f,g)) . (h . x) )
assume A24: x in dom (G * (g,f)) ; ::_thesis: (G * (g,f)) . x = (G * (f,g)) . (h . x)
then consider y, z being set  such that
A25: x = [y,z] by RELAT_1:def_1;
reconsider z = z as Element of I by A17, A24, A25, ZFMISC_1:87;
reconsider y = y as Element of J by A17, A24, A25, ZFMISC_1:87;
A26: [z,y] in dom (G * (f,g)) by A18, ZFMISC_1:87;
A27: [y,z] in dom (G * (g,f)) by A17, ZFMISC_1:87;
thus (G * (f,g)) . (h . x) = (G * (f,g)) . (h . (y,z)) by A25
.= (G * (f,g)) . (z,y) by A2
.= G . ((f . z),(g . y)) by A26, FINSEQOP:77
.= G . ((g . y),(f . z)) by A15, BINOP_1:def_2
.= (G * (g,f)) . (y,z) by A27, FINSEQOP:77
.= (G * (g,f)) . x by A25 ; ::_thesis: verum
end;
hence  G * (g,f) = (G * (f,g)) * h by A19, FUNCT_1:10; ::_thesis: verum
end;
A28: ( X c= I & Y c= J ) by FINSUB_1:def_5;
 for y being set holds
( y in [:X,Y:] iff y in h .: [:Y,X:] )
proof
let y be set ; ::_thesis: ( y in [:X,Y:] iff y in h .: [:Y,X:] )
thus  ( y in [:X,Y:] implies y in h .: [:Y,X:] ) ::_thesis: ( y in h .: [:Y,X:] implies y in [:X,Y:] )
proof
assume A29: y in [:X,Y:] ; ::_thesis: y in h .: [:Y,X:]
then consider y1, x1 being set  such that
A30: y = [y1,x1] by RELAT_1:def_1;
A31: ( y1 in X & x1 in Y ) by A29, A30, ZFMISC_1:87;
then A32: ( [x1,y1] in [:Y,X:] & [x1,y1] in dom h ) by A28, A2, ZFMISC_1:87;
 h . (x1,y1) = y by A28, A2, A30, A31;
hence  y in h .: [:Y,X:] by A32, FUNCT_1:def_6; ::_thesis: verum
end;
assume  y in h .: [:Y,X:] ; ::_thesis: y in [:X,Y:]
then consider x being set  such that
 x in dom h and
A33: x in [:Y,X:] and
A34: y = h . x by FUNCT_1:def_6;
consider x1, y1 being set  such that
A35: x = [x1,y1] by A33, RELAT_1:def_1;
A36: ( x1 in Y & y1 in X ) by A33, A35, ZFMISC_1:87;
 y = h . (x1,y1) by A34, A35;
then  y = [y1,x1] by A28, A2, A36;
hence  y in [:X,Y:] by A36, ZFMISC_1:87; ::_thesis: verum
end;
then A37: h .: [:Y,X:] = [:X,Y:] by TARSKI:1;
reconsider h = h as Function of [:J,I:],[:I,J:] by A2, A11, FUNCT_2:3;
F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],((G * (f,g)) * h)) by A1, A10, A37, SETWOP_2:6
.= F $$ ([:Y,X:],(G * (g,f))) by A16 ;
hence  F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f))) ; ::_thesis: verum
end;

theorem Th24: :: MATRIX_3:24
for D, I, J being non empty set
for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D st F is commutative & F is associative holds
for x being Element of I
for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ ({.y.},g)))))
proof
let D be non empty set ; ::_thesis: for I, J being non empty set
for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D st F is commutative & F is associative holds
for x being Element of I
for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ ({.y.},g)))))
let I, J be non empty set ; ::_thesis: for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D st F is commutative & F is associative holds
for x being Element of I
for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ ({.y.},g)))))
let F, G be BinOp of D; ::_thesis: for f being Function of I,D
for g being Function of J,D st F is commutative & F is associative holds
for x being Element of I
for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ ({.y.},g)))))
let f be Function of I,D; ::_thesis: for g being Function of J,D st F is commutative & F is associative holds
for x being Element of I
for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ ({.y.},g)))))
let g be Function of J,D; ::_thesis: ( F is commutative & F is associative implies for x being Element of I
for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ ({.y.},g))))) )
assume A1: ( F is commutative & F is associative ) ; ::_thesis: for x being Element of I
for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ ({.y.},g)))))
reconsider G = G as Function of [:D,D:],D ;
A2: dom (G * (f,g)) = [:I,J:] by FUNCT_2:def_1;
now__::_thesis:_for_x_being_Element_of_I
for_y_being_Element_of_J_holds_F_$$_([:{.x.},{.y.}:],(G_*_(f,g)))_=_F_$$_({.x.},(G_[:]_(f,(F_$$_({.y.},g)))))
let x be Element of I; ::_thesis: for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ ({.y.},g)))))
let y be Element of J; ::_thesis: F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ ({.y.},g)))))
A3: [x,y] in [:I,J:] by ZFMISC_1:87;
reconsider z = g . y as Element of D ;
reconsider u = [x,y] as Element of [:I,J:] by ZFMISC_1:87;
A4: dom <:f,((dom f) --> z):> = (dom f) /\ (dom ((dom f) --> z)) by FUNCT_3:def_7
.= (dom f) /\ (dom f) by FUNCOP_1:13
.= dom f ;
 ( rng f c= D & rng ((dom f) --> z) c= D ) by RELAT_1:def_19;
then A5: [:(rng f),(rng ((dom f) --> z)):] c= [:D,D:] by ZFMISC_1:96;
 dom f = I by FUNCT_2:def_1;
then A6: x in dom <:f,((dom f) --> z):> by A4;
 ( dom G = [:D,D:] & rng <:f,((dom f) --> z):> c= [:(rng f),(rng ((dom f) --> z)):] ) by FUNCT_2:def_1, FUNCT_3:51;
then  x in dom (G * <:f,((dom f) --> z):>) by A6, A5, RELAT_1:27, XBOOLE_1:1;
then A7: x in dom (G [:] (f,z)) by FUNCOP_1:def_4;
A8: F $$ ({.x.},(G [:] (f,(F $$ ({.y.},g))))) = (G [:] (f,(F $$ ({.y.},g)))) . x by A1, SETWISEO:17
.= (G [:] (f,(g . y))) . x by A1, SETWISEO:17
.= G . ((f . x),(g . y)) by A7, FUNCOP_1:27 ;
F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.u.},(G * (f,g))) by ZFMISC_1:29
.= (G * (f,g)) . (x,y) by A1, SETWISEO:17
.= G . ((f . x),(g . y)) by A2, A3, FINSEQOP:77 ;
hence  F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ ({.y.},g))))) by A8; ::_thesis: verum
end;
hence  for x being Element of I
for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ ({.y.},g))))) ; ::_thesis: verum
end;

theorem Th25: :: MATRIX_3:25
for D, I, J being non empty set
for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
for x being Element of I holds F $$ ([:{.x.},Y:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ (Y,g)))))
proof
let D be non empty set ; ::_thesis: for I, J being non empty set
for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
for x being Element of I holds F $$ ([:{.x.},Y:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ (Y,g)))))
let I, J be non empty set ; ::_thesis: for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
for x being Element of I holds F $$ ([:{.x.},Y:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ (Y,g)))))
let F, G be BinOp of D; ::_thesis: for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
for x being Element of I holds F $$ ([:{.x.},Y:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ (Y,g)))))
let f be Function of I,D; ::_thesis: for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
for x being Element of I holds F $$ ([:{.x.},Y:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ (Y,g)))))
let g be Function of J,D; ::_thesis: for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
for x being Element of I holds F $$ ([:{.x.},Y:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ (Y,g)))))
let X be Element of Fin I; ::_thesis: for Y being Element of Fin J st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
for x being Element of I holds F $$ ([:{.x.},Y:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ (Y,g)))))
let Y be Element of Fin J; ::_thesis: ( F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F implies for x being Element of I holds F $$ ([:{.x.},Y:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ (Y,g))))) )
assume that
A1: F is commutative and
A2: F is associative and
A3: F is having_a_unity and
A4: F is having_an_inverseOp and
A5: G is_distributive_wrt F ; ::_thesis: for x being Element of I holds F $$ ([:{.x.},Y:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ (Y,g)))))
now__::_thesis:_for_x_being_Element_of_I
for_Y_being_Element_of_Fin_J_holds_S1[Y]
let x be Element of I; ::_thesis: for Y being Element of Fin J holds S1[Y]
defpred S1[ Element of Fin J] means F $$ ([:{.x.},$1:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ ($1,g)))));
A6: S1[ {}. J]
proof
set z = the_unity_wrt F;
reconsider T = {}. [:I,J:] as Element of Fin [:I,J:] ;
A7: T = [:{x},({}. J):] by ZFMISC_1:90;
A8: dom <:f,((dom f) --> (the_unity_wrt F)):> = (dom f) /\ (dom ((dom f) --> (the_unity_wrt F))) by FUNCT_3:def_7
.= (dom f) /\ (dom f) by FUNCOP_1:13
.= dom f ;
 ( rng f c= D & rng ((dom f) --> (the_unity_wrt F)) c= D ) by RELAT_1:def_19;
then A9: [:(rng f),(rng ((dom f) --> (the_unity_wrt F))):] c= [:D,D:] by ZFMISC_1:96;
 dom f = I by FUNCT_2:def_1;
then A10: x in dom <:f,((dom f) --> (the_unity_wrt F)):> by A8;
 ( dom G = [:D,D:] & rng <:f,((dom f) --> (the_unity_wrt F)):> c= [:(rng f),(rng ((dom f) --> (the_unity_wrt F))):] ) by FUNCT_2:def_1, FUNCT_3:51;
then  x in dom (G * <:f,((dom f) --> (the_unity_wrt F)):>) by A10, A9, RELAT_1:27, XBOOLE_1:1;
then A11: x in dom (G [:] (f,(the_unity_wrt F))) by FUNCOP_1:def_4;
F $$ ({.x.},(G [:] (f,(F $$ (({}. J),g))))) = F $$ ({.x.},(G [:] (f,(the_unity_wrt F)))) by A1, A2, A3, SETWISEO:31
.= (G [:] (f,(the_unity_wrt F))) . x by A1, A2, SETWISEO:17
.= G . ((f . x),(the_unity_wrt F)) by A11, FUNCOP_1:27
.= the_unity_wrt F by A2, A3, A4, A5, FINSEQOP:66 ;
hence  S1[ {}. J] by A1, A2, A3, A7, SETWISEO:31; ::_thesis: verum
end;
A12: for Y1 being Element of Fin J
for y being Element of J st S1[Y1] holds
S1[Y1 \/ {.y.}]
proof
let Y1 be Element of Fin J; ::_thesis: for y being Element of J st S1[Y1] holds
S1[Y1 \/ {.y.}]
let y be Element of J; ::_thesis: ( S1[Y1] implies S1[Y1 \/ {.y.}] )
assume A13: F $$ ([:{.x.},Y1:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ (Y1,g))))) ; ::_thesis: S1[Y1 \/ {.y.}]
reconsider s = {.y.} as Element of Fin J ;
percases ( y in Y1 or not y in Y1 ) ;
suppose y in Y1 ; ::_thesis: S1[Y1 \/ {.y.}]
then  Y1 \/ {y} = Y1 by ZFMISC_1:40;
hence  S1[Y1 \/ {.y.}] by A13; ::_thesis: verum
end;
suppose not y in Y1 ; ::_thesis: S1[Y1 \/ {.y.}]
then A14: Y1 misses {y} by ZFMISC_1:50;
then A15: [:{x},Y1:] misses [:{x},s:] by ZFMISC_1:104;
thus F $$ ([:{.x.},(Y1 \/ {.y.}):],(G * (f,g))) = F $$ (([:{.x.},Y1:] \/ [:{.x.},s:]),(G * (f,g))) by ZFMISC_1:97
.= F . ((F $$ ([:{.x.},Y1:],(G * (f,g)))),(F $$ ([:{.x.},s:],(G * (f,g))))) by A1, A2, A3, A15, SETWOP_2:4
.= F . ((F $$ ({.x.},(G [:] (f,(F $$ (Y1,g)))))),(F $$ ({.x.},(G [:] (f,(F $$ (s,g))))))) by A1, A2, A13, Th24
.= F $$ ({.x.},(F .: ((G [:] (f,(F $$ (Y1,g)))),(G [:] (f,(F $$ (s,g))))))) by A1, A2, A3, SETWOP_2:10
.= F $$ ({.x.},(G [:] (f,(F . ((F $$ (Y1,g)),(F $$ (s,g))))))) by A5, FINSEQOP:36
.= F $$ ({.x.},(G [:] (f,(F $$ ((Y1 \/ {.y.}),g))))) by A1, A2, A3, A14, SETWOP_2:4 ; ::_thesis: verum
end;
end;
end;
thus  for Y being Element of Fin J holds S1[Y] from SETWISEO:sch_4(A6, A12); ::_thesis: verum
end;
hence  for x being Element of I holds F $$ ([:{.x.},Y:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ (Y,g))))) ; ::_thesis: verum
end;

theorem Th26: :: MATRIX_3:26
for D, I, J being non empty set
for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (X,(G [:] (f,(F $$ (Y,g)))))
proof
let D be non empty set ; ::_thesis: for I, J being non empty set
for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (X,(G [:] (f,(F $$ (Y,g)))))
let I, J be non empty set ; ::_thesis: for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (X,(G [:] (f,(F $$ (Y,g)))))
let F, G be BinOp of D; ::_thesis: for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (X,(G [:] (f,(F $$ (Y,g)))))
let f be Function of I,D; ::_thesis: for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (X,(G [:] (f,(F $$ (Y,g)))))
let g be Function of J,D; ::_thesis: for X being Element of Fin I
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (X,(G [:] (f,(F $$ (Y,g)))))
let X be Element of Fin I; ::_thesis: for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (X,(G [:] (f,(F $$ (Y,g)))))
let Y be Element of Fin J; ::_thesis: ( F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F implies F $$ ([:X,Y:],(G * (f,g))) = F $$ (X,(G [:] (f,(F $$ (Y,g))))) )
assume that
A1: ( F is having_a_unity & F is commutative & F is associative ) and
A2: ( F is having_an_inverseOp & G is_distributive_wrt F ) ; ::_thesis: F $$ ([:X,Y:],(G * (f,g))) = F $$ (X,(G [:] (f,(F $$ (Y,g)))))
defpred S1[ Element of Fin I] means F $$ ([:$1,Y:],(G * (f,g))) = F $$ ($1,(G [:] (f,(F $$ (Y,g)))));
A3: for X1 being Element of Fin I
for x being Element of I st S1[X1] holds
S1[X1 \/ {.x.}]
proof
let X1 be Element of Fin I; ::_thesis: for x being Element of I st S1[X1] holds
S1[X1 \/ {.x.}]
let x be Element of I; ::_thesis: ( S1[X1] implies S1[X1 \/ {.x.}] )
reconsider s = {.x.} as Element of Fin I ;
assume A4: F $$ ([:X1,Y:],(G * (f,g))) = F $$ (X1,(G [:] (f,(F $$ (Y,g))))) ; ::_thesis: S1[X1 \/ {.x.}]
now__::_thesis:_(_(_x_in_X1_&_S1[X1_\/_{.x.}]_)_or_(_not_x_in_X1_&_F_$$_([:(X1_\/_{.x.}),Y:],(G_*_(f,g)))_=_F_$$_((X1_\/_{.x.}),(G_[:]_(f,(F_$$_(Y,g)))))_)_)
percases ( x in X1 or not x in X1 ) ;
case x in X1 ; ::_thesis: S1[X1 \/ {.x.}]
then  X1 \/ {x} = X1 by ZFMISC_1:40;
hence  S1[X1 \/ {.x.}] by A4; ::_thesis: verum
end;
case not x in X1 ; ::_thesis: F $$ ([:(X1 \/ {.x.}),Y:],(G * (f,g))) = F $$ ((X1 \/ {.x.}),(G [:] (f,(F $$ (Y,g)))))
then A5: X1 misses {x} by ZFMISC_1:50;
then A6: [:X1,Y:] misses [:s,Y:] by ZFMISC_1:104;
thus F $$ ([:(X1 \/ {.x.}),Y:],(G * (f,g))) = F $$ (([:X1,Y:] \/ [:s,Y:]),(G * (f,g))) by ZFMISC_1:97
.= F . ((F $$ ([:X1,Y:],(G * (f,g)))),(F $$ ([:s,Y:],(G * (f,g))))) by A1, A6, SETWOP_2:4
.= F . ((F $$ (X1,(G [:] (f,(F $$ (Y,g)))))),(F $$ (s,(G [:] (f,(F $$ (Y,g))))))) by A1, A2, A4, Th25
.= F $$ ((X1 \/ {.x.}),(G [:] (f,(F $$ (Y,g))))) by A1, A5, SETWOP_2:4 ; ::_thesis: verum
end;
end;
end;
hence  S1[X1 \/ {.x.}] ; ::_thesis: verum
end;
A7: S1[ {}. I]
proof
reconsider T = {}. [:I,J:] as Element of Fin [:I,J:] ;
 T = [:({}. I),Y:] by ZFMISC_1:90;
then  F $$ ([:({}. I),Y:],(G * (f,g))) = the_unity_wrt F by A1, SETWISEO:31;
hence  S1[ {}. I] by A1, SETWISEO:31; ::_thesis: verum
end;
 for X1 being Element of Fin I holds S1[X1] from SETWISEO:sch_4(A7, A3);
hence  F $$ ([:X,Y:],(G * (f,g))) = F $$ (X,(G [:] (f,(F $$ (Y,g))))) ; ::_thesis: verum
end;

theorem :: MATRIX_3:27
for D, I, J being non empty set
for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D st F is commutative & F is associative & G is commutative holds
for x being Element of I
for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.y.},(G [;] ((F $$ ({.x.},f)),g)))
proof
let D be non empty set ; ::_thesis: for I, J being non empty set
for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D st F is commutative & F is associative & G is commutative holds
for x being Element of I
for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.y.},(G [;] ((F $$ ({.x.},f)),g)))
let I, J be non empty set ; ::_thesis: for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D st F is commutative & F is associative & G is commutative holds
for x being Element of I
for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.y.},(G [;] ((F $$ ({.x.},f)),g)))
let F, G be BinOp of D; ::_thesis: for f being Function of I,D
for g being Function of J,D st F is commutative & F is associative & G is commutative holds
for x being Element of I
for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.y.},(G [;] ((F $$ ({.x.},f)),g)))
let f be Function of I,D; ::_thesis: for g being Function of J,D st F is commutative & F is associative & G is commutative holds
for x being Element of I
for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.y.},(G [;] ((F $$ ({.x.},f)),g)))
let g be Function of J,D; ::_thesis: ( F is commutative & F is associative & G is commutative implies for x being Element of I
for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.y.},(G [;] ((F $$ ({.x.},f)),g))) )
assume that
A1: ( F is commutative & F is associative ) and
A2: G is commutative ; ::_thesis: for x being Element of I
for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.y.},(G [;] ((F $$ ({.x.},f)),g)))
now__::_thesis:_for_x_being_Element_of_I
for_y_being_Element_of_J_holds_F_$$_([:{.x.},{.y.}:],(G_*_(f,g)))_=_F_$$_({.y.},(G_[;]_((F_$$_({.x.},f)),g)))
let x be Element of I; ::_thesis: for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.y.},(G [;] ((F $$ ({.x.},f)),g)))
let y be Element of J; ::_thesis: F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.y.},(G [;] ((F $$ ({.x.},f)),g)))
thus F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ([:{.y.},{.x.}:],(G * (g,f))) by A1, A2, Th23
.= F $$ ({.y.},(G [:] (g,(F $$ ({.x.},f))))) by A1, Th24
.= F $$ ({.y.},(G [;] ((F $$ ({.x.},f)),g))) by A2, FUNCOP_1:64 ; ::_thesis: verum
end;
hence  for x being Element of I
for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.y.},(G [;] ((F $$ ({.x.},f)),g))) ; ::_thesis: verum
end;

theorem :: MATRIX_3:28
for D, I, J being non empty set
for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (Y,(G [;] ((F $$ (X,f)),g)))
proof
let D be non empty set ; ::_thesis: for I, J being non empty set
for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (Y,(G [;] ((F $$ (X,f)),g)))
let I, J be non empty set ; ::_thesis: for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (Y,(G [;] ((F $$ (X,f)),g)))
let F, G be BinOp of D; ::_thesis: for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (Y,(G [;] ((F $$ (X,f)),g)))
let f be Function of I,D; ::_thesis: for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (Y,(G [;] ((F $$ (X,f)),g)))
let g be Function of J,D; ::_thesis: for X being Element of Fin I
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (Y,(G [;] ((F $$ (X,f)),g)))
let X be Element of Fin I; ::_thesis: for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (Y,(G [;] ((F $$ (X,f)),g)))
let Y be Element of Fin J; ::_thesis: ( F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F & G is commutative implies F $$ ([:X,Y:],(G * (f,g))) = F $$ (Y,(G [;] ((F $$ (X,f)),g))) )
assume that
A1: ( F is having_a_unity & F is commutative & F is associative ) and
A2: ( F is having_an_inverseOp & G is_distributive_wrt F ) and
A3: G is commutative ; ::_thesis: F $$ ([:X,Y:],(G * (f,g))) = F $$ (Y,(G [;] ((F $$ (X,f)),g)))
thus F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f))) by A1, A3, Th23
.= F $$ (Y,(G [:] (g,(F $$ (X,f))))) by A1, A2, Th26
.= F $$ (Y,(G [;] ((F $$ (X,f)),g))) by A3, FUNCOP_1:64 ; ::_thesis: verum
end;

theorem Th29: :: MATRIX_3:29
for D, I, J being non empty set
for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of I,D
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative holds
for x being Element of I st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) holds
F $$ ([:{.x.},Y:],f) = F $$ ({.x.},g)
proof
let D be non empty set ; ::_thesis: for I, J being non empty set
for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of I,D
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative holds
for x being Element of I st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) holds
F $$ ([:{.x.},Y:],f) = F $$ ({.x.},g)
let I, J be non empty set ; ::_thesis: for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of I,D
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative holds
for x being Element of I st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) holds
F $$ ([:{.x.},Y:],f) = F $$ ({.x.},g)
let F be BinOp of D; ::_thesis: for f being Function of [:I,J:],D
for g being Function of I,D
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative holds
for x being Element of I st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) holds
F $$ ([:{.x.},Y:],f) = F $$ ({.x.},g)
let f be Function of [:I,J:],D; ::_thesis: for g being Function of I,D
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative holds
for x being Element of I st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) holds
F $$ ([:{.x.},Y:],f) = F $$ ({.x.},g)
let g be Function of I,D; ::_thesis: for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative holds
for x being Element of I st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) holds
F $$ ([:{.x.},Y:],f) = F $$ ({.x.},g)
let Y be Element of Fin J; ::_thesis: ( F is having_a_unity & F is commutative & F is associative implies for x being Element of I st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) holds
F $$ ([:{.x.},Y:],f) = F $$ ({.x.},g) )
assume that
A1: F is having_a_unity and
A2: ( F is commutative & F is associative ) ; ::_thesis: for x being Element of I st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) holds
F $$ ([:{.x.},Y:],f) = F $$ ({.x.},g)
now__::_thesis:_for_x_being_Element_of_I_st_(_for_i_being_Element_of_I_holds_g_._i_=_F_$$_(Y,((curry_f)_._i))_)_holds_
F_$$_([:{.x.},Y:],f)_=_F_$$_({.x.},g)
let x be Element of I; ::_thesis: ( ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) implies F $$ ([:{.x.},Y:],f) = F $$ ({.x.},g) )
assume A3: for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ; ::_thesis: F $$ ([:{.x.},Y:],f) = F $$ ({.x.},g)
deffunc H1( set ) ->  set = [x,$1];
consider h being Function such that
A4: ( dom h = J & ( for y being set st y in J holds
h . y = H1(y) ) ) from FUNCT_1:sch_3();
A5: ( dom ((curry f) . x) = J & dom (f * h) = J & rng h c= [:I,J:] )
proof
A6: dom f = [:I,J:] by FUNCT_2:def_1;
then  ex g being Function st
( g = (curry f) . x & dom g = J & rng g c= rng f & ( for y being set st y in J holds
g . y = f . (x,y) ) ) by FUNCT_5:29;
hence  dom ((curry f) . x) = J ; ::_thesis: ( dom (f * h) = J & rng h c= [:I,J:] )
now__::_thesis:_for_y_being_set_st_y_in_rng_h_holds_
y_in_dom_f
let y be set ; ::_thesis: ( y in rng h implies y in dom f )
assume  y in rng h ; ::_thesis: y in dom f
then consider z being set  such that
A7: z in dom h and
A8: y = h . z by FUNCT_1:def_3;
 y = [x,z] by A4, A7, A8;
hence  y in dom f by A4, A6, A7, ZFMISC_1:87; ::_thesis: verum
end;
then  rng h c= dom f by TARSKI:def_3;
hence  ( dom (f * h) = J & rng h c= [:I,J:] ) by A4, FUNCT_2:def_1, RELAT_1:27; ::_thesis: verum
end;
A9: for y being set st y in J holds
((curry f) . x) . y = (f * h) . y
proof
let y be set ; ::_thesis: ( y in J implies ((curry f) . x) . y = (f * h) . y )
 dom f = [:I,J:] by FUNCT_2:def_1;
then A10: ex g being Function st
( g = (curry f) . x & dom g = J & rng g c= rng f & ( for y being set st y in J holds
g . y = f . (x,y) ) ) by FUNCT_5:29;
assume A11: y in J ; ::_thesis: ((curry f) . x) . y = (f * h) . y
hence (f * h) . y = f . (h . y) by A5, FUNCT_1:12
.= f . (x,y) by A4, A11
.= ((curry f) . x) . y by A11, A10 ;
::_thesis: verum
end;
 for y being set holds
( y in [:{x},Y:] iff y in h .: Y )
proof
let y be set ; ::_thesis: ( y in [:{x},Y:] iff y in h .: Y )
thus  ( y in [:{x},Y:] implies y in h .: Y ) ::_thesis: ( y in h .: Y implies y in [:{x},Y:] )
proof
assume A12: y in [:{x},Y:] ; ::_thesis: y in h .: Y
then consider y1, x1 being set  such that
A13: y = [y1,x1] by RELAT_1:def_1;
A14: y1 in {x} by A12, A13, ZFMISC_1:87;
A15: ( Y c= J & x1 in Y ) by A12, A13, FINSUB_1:def_5, ZFMISC_1:87;
then h . x1 = [x,x1] by A4
.= y by A13, A14, TARSKI:def_1 ;
hence  y in h .: Y by A4, A15, FUNCT_1:def_6; ::_thesis: verum
end;
assume  y in h .: Y ; ::_thesis: y in [:{x},Y:]
then consider z being set  such that
A16: z in dom h and
A17: z in Y and
A18: y = h . z by FUNCT_1:def_6;
 y = [x,z] by A4, A16, A18;
hence  y in [:{x},Y:] by A17, ZFMISC_1:105; ::_thesis: verum
end;
then A19: h .: Y = [:{x},Y:] by TARSKI:1;
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_h_&_x2_in_dom_h_&_h_._x1_=_h_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom h & x2 in dom h & h . x1 = h . x2 implies x1 = x2 )
assume that
A20: x1 in dom h and
A21: x2 in dom h and
A22: h . x1 = h . x2 ; ::_thesis: x1 = x2
[x,x1] = h . x2 by A4, A20, A22
.= [x,x2] by A4, A21 ;
hence  x1 = x2 by XTUPLE_0:1; ::_thesis: verum
end;
then A23: h is one-to-one by FUNCT_1:def_4;
reconsider h = h as Function of J,[:I,J:] by A4, A5, FUNCT_2:2;
thus F $$ ([:{.x.},Y:],f) = F $$ (Y,(f * h)) by A1, A2, A23, A19, SETWOP_2:6
.= F $$ (Y,((curry f) . x)) by A5, A9, FUNCT_1:2
.= g . x by A3
.= F $$ ({.x.},g) by A2, SETWISEO:17 ; ::_thesis: verum
end;
hence  for x being Element of I st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) holds
F $$ ([:{.x.},Y:],f) = F $$ ({.x.},g) ; ::_thesis: verum
end;

theorem Th30: :: MATRIX_3:30
for D, I, J being non empty set
for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of I,D
for X being Element of Fin I
for Y being Element of Fin J st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) & F is having_a_unity & F is commutative & F is associative holds
F $$ ([:X,Y:],f) = F $$ (X,g)
proof
let D be non empty set ; ::_thesis: for I, J being non empty set
for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of I,D
for X being Element of Fin I
for Y being Element of Fin J st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) & F is having_a_unity & F is commutative & F is associative holds
F $$ ([:X,Y:],f) = F $$ (X,g)
let I, J be non empty set ; ::_thesis: for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of I,D
for X being Element of Fin I
for Y being Element of Fin J st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) & F is having_a_unity & F is commutative & F is associative holds
F $$ ([:X,Y:],f) = F $$ (X,g)
let F be BinOp of D; ::_thesis: for f being Function of [:I,J:],D
for g being Function of I,D
for X being Element of Fin I
for Y being Element of Fin J st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) & F is having_a_unity & F is commutative & F is associative holds
F $$ ([:X,Y:],f) = F $$ (X,g)
let f be Function of [:I,J:],D; ::_thesis: for g being Function of I,D
for X being Element of Fin I
for Y being Element of Fin J st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) & F is having_a_unity & F is commutative & F is associative holds
F $$ ([:X,Y:],f) = F $$ (X,g)
let g be Function of I,D; ::_thesis: for X being Element of Fin I
for Y being Element of Fin J st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) & F is having_a_unity & F is commutative & F is associative holds
F $$ ([:X,Y:],f) = F $$ (X,g)
let X be Element of Fin I; ::_thesis: for Y being Element of Fin J st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) & F is having_a_unity & F is commutative & F is associative holds
F $$ ([:X,Y:],f) = F $$ (X,g)
let Y be Element of Fin J; ::_thesis: ( ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) & F is having_a_unity & F is commutative & F is associative implies F $$ ([:X,Y:],f) = F $$ (X,g) )
assume that
A1: for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) and
A2: ( F is having_a_unity & F is commutative & F is associative ) ; ::_thesis: F $$ ([:X,Y:],f) = F $$ (X,g)
defpred S1[ Element of Fin I] means F $$ ([:$1,Y:],f) = F $$ ($1,g);
A3: for X1 being Element of Fin I
for x being Element of I st S1[X1] holds
S1[X1 \/ {.x.}]
proof
let X1 be Element of Fin I; ::_thesis: for x being Element of I st S1[X1] holds
S1[X1 \/ {.x.}]
let x be Element of I; ::_thesis: ( S1[X1] implies S1[X1 \/ {.x.}] )
assume A4: F $$ ([:X1,Y:],f) = F $$ (X1,g) ; ::_thesis: S1[X1 \/ {.x.}]
reconsider s = {.x.} as Element of Fin I ;
percases ( x in X1 or not x in X1 ) ;
suppose x in X1 ; ::_thesis: S1[X1 \/ {.x.}]
then  X1 \/ {x} = X1 by ZFMISC_1:40;
hence  S1[X1 \/ {.x.}] by A4; ::_thesis: verum
end;
suppose not x in X1 ; ::_thesis: S1[X1 \/ {.x.}]
then A5: X1 misses {x} by ZFMISC_1:50;
then A6: [:X1,Y:] misses [:s,Y:] by ZFMISC_1:104;
thus F $$ ([:(X1 \/ {.x.}),Y:],f) = F $$ (([:X1,Y:] \/ [:s,Y:]),f) by ZFMISC_1:97
.= F . ((F $$ ([:X1,Y:],f)),(F $$ ([:s,Y:],f))) by A2, A6, SETWOP_2:4
.= F . ((F $$ (X1,g)),(F $$ (s,g))) by A1, A2, A4, Th29
.= F $$ ((X1 \/ {.x.}),g) by A2, A5, SETWOP_2:4 ; ::_thesis: verum
end;
end;
end;
A7: S1[ {}. I]
proof
reconsider T = {}. [:I,J:] as Element of Fin [:I,J:] ;
 T = [:({}. I),Y:] by ZFMISC_1:90;
then  F $$ ([:({}. I),Y:],f) = the_unity_wrt F by A2, SETWISEO:31;
hence  S1[ {}. I] by A2, SETWISEO:31; ::_thesis: verum
end;
 for X1 being Element of Fin I holds S1[X1] from SETWISEO:sch_4(A7, A3);
hence  F $$ ([:X,Y:],f) = F $$ (X,g) ; ::_thesis: verum
end;

theorem Th31: :: MATRIX_3:31
for D, I, J being non empty set
for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of J,D
for X being Element of Fin I st F is having_a_unity & F is commutative & F is associative holds
for y being Element of J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) holds
F $$ ([:X,{.y.}:],f) = F $$ ({.y.},g)
proof
let D be non empty set ; ::_thesis: for I, J being non empty set
for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of J,D
for X being Element of Fin I st F is having_a_unity & F is commutative & F is associative holds
for y being Element of J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) holds
F $$ ([:X,{.y.}:],f) = F $$ ({.y.},g)
let I, J be non empty set ; ::_thesis: for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of J,D
for X being Element of Fin I st F is having_a_unity & F is commutative & F is associative holds
for y being Element of J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) holds
F $$ ([:X,{.y.}:],f) = F $$ ({.y.},g)
let F be BinOp of D; ::_thesis: for f being Function of [:I,J:],D
for g being Function of J,D
for X being Element of Fin I st F is having_a_unity & F is commutative & F is associative holds
for y being Element of J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) holds
F $$ ([:X,{.y.}:],f) = F $$ ({.y.},g)
let f be Function of [:I,J:],D; ::_thesis: for g being Function of J,D
for X being Element of Fin I st F is having_a_unity & F is commutative & F is associative holds
for y being Element of J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) holds
F $$ ([:X,{.y.}:],f) = F $$ ({.y.},g)
let g be Function of J,D; ::_thesis: for X being Element of Fin I st F is having_a_unity & F is commutative & F is associative holds
for y being Element of J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) holds
F $$ ([:X,{.y.}:],f) = F $$ ({.y.},g)
let X be Element of Fin I; ::_thesis: ( F is having_a_unity & F is commutative & F is associative implies for y being Element of J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) holds
F $$ ([:X,{.y.}:],f) = F $$ ({.y.},g) )
assume that
A1: F is having_a_unity and
A2: ( F is commutative & F is associative ) ; ::_thesis: for y being Element of J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) holds
F $$ ([:X,{.y.}:],f) = F $$ ({.y.},g)
now__::_thesis:_for_y_being_Element_of_J_st_(_for_j_being_Element_of_J_holds_g_._j_=_F_$$_(X,((curry'_f)_._j))_)_holds_
F_$$_([:X,{.y.}:],f)_=_F_$$_({.y.},g)
let y be Element of J; ::_thesis: ( ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) implies F $$ ([:X,{.y.}:],f) = F $$ ({.y.},g) )
assume A3: for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ; ::_thesis: F $$ ([:X,{.y.}:],f) = F $$ ({.y.},g)
deffunc H1( set ) ->  set = [$1,y];
consider h being Function such that
A4: ( dom h = I & ( for x being set st x in I holds
h . x = H1(x) ) ) from FUNCT_1:sch_3();
A5: ( dom ((curry' f) . y) = I & dom (f * h) = I & rng h c= [:I,J:] )
proof
A6: dom f = [:I,J:] by FUNCT_2:def_1;
then  ex g being Function st
( g = (curry' f) . y & dom g = I & rng g c= rng f & ( for x being set st x in I holds
g . x = f . (x,y) ) ) by FUNCT_5:32;
hence  dom ((curry' f) . y) = I ; ::_thesis: ( dom (f * h) = I & rng h c= [:I,J:] )
now__::_thesis:_for_x_being_set_st_x_in_rng_h_holds_
x_in_dom_f
let x be set ; ::_thesis: ( x in rng h implies x in dom f )
assume  x in rng h ; ::_thesis: x in dom f
then consider z being set  such that
A7: z in dom h and
A8: x = h . z by FUNCT_1:def_3;
 x = [z,y] by A4, A7, A8;
hence  x in dom f by A4, A6, A7, ZFMISC_1:87; ::_thesis: verum
end;
then  rng h c= dom f by TARSKI:def_3;
hence  ( dom (f * h) = I & rng h c= [:I,J:] ) by A4, FUNCT_2:def_1, RELAT_1:27; ::_thesis: verum
end;
A9: for x being set st x in I holds
((curry' f) . y) . x = (f * h) . x
proof
let x be set ; ::_thesis: ( x in I implies ((curry' f) . y) . x = (f * h) . x )
 dom f = [:I,J:] by FUNCT_2:def_1;
then A10: ex g being Function st
( g = (curry' f) . y & dom g = I & rng g c= rng f & ( for x being set st x in I holds
g . x = f . (x,y) ) ) by FUNCT_5:32;
assume A11: x in I ; ::_thesis: ((curry' f) . y) . x = (f * h) . x
hence (f * h) . x = f . (h . x) by A5, FUNCT_1:12
.= f . (x,y) by A4, A11
.= ((curry' f) . y) . x by A11, A10 ;
::_thesis: verum
end;
 for x being set holds
( x in [:X,{y}:] iff x in h .: X )
proof
let x be set ; ::_thesis: ( x in [:X,{y}:] iff x in h .: X )
thus  ( x in [:X,{y}:] implies x in h .: X ) ::_thesis: ( x in h .: X implies x in [:X,{y}:] )
proof
assume A12: x in [:X,{y}:] ; ::_thesis: x in h .: X
then consider x1, y1 being set  such that
A13: x = [x1,y1] by RELAT_1:def_1;
A14: y1 in {y} by A12, A13, ZFMISC_1:87;
A15: ( X c= I & x1 in X ) by A12, A13, FINSUB_1:def_5, ZFMISC_1:87;
then h . x1 = [x1,y] by A4
.= x by A13, A14, TARSKI:def_1 ;
hence  x in h .: X by A4, A15, FUNCT_1:def_6; ::_thesis: verum
end;
assume  x in h .: X ; ::_thesis: x in [:X,{y}:]
then consider z being set  such that
A16: z in dom h and
A17: z in X and
A18: x = h . z by FUNCT_1:def_6;
 x = [z,y] by A4, A16, A18;
hence  x in [:X,{y}:] by A17, ZFMISC_1:106; ::_thesis: verum
end;
then A19: h .: X = [:X,{y}:] by TARSKI:1;
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_h_&_x2_in_dom_h_&_h_._x1_=_h_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom h & x2 in dom h & h . x1 = h . x2 implies x1 = x2 )
assume that
A20: x1 in dom h and
A21: x2 in dom h and
A22: h . x1 = h . x2 ; ::_thesis: x1 = x2
[x1,y] = h . x2 by A4, A20, A22
.= [x2,y] by A4, A21 ;
hence  x1 = x2 by XTUPLE_0:1; ::_thesis: verum
end;
then A23: h is one-to-one by FUNCT_1:def_4;
reconsider h = h as Function of I,[:I,J:] by A4, A5, FUNCT_2:2;
thus F $$ ([:X,{.y.}:],f) = F $$ (X,(f * h)) by A1, A2, A23, A19, SETWOP_2:6
.= F $$ (X,((curry' f) . y)) by A5, A9, FUNCT_1:2
.= g . y by A3
.= F $$ ({.y.},g) by A2, SETWISEO:17 ; ::_thesis: verum
end;
hence  for y being Element of J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) holds
F $$ ([:X,{.y.}:],f) = F $$ ({.y.},g) ; ::_thesis: verum
end;

theorem Th32: :: MATRIX_3:32
for D, I, J being non empty set
for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) & F is having_a_unity & F is commutative & F is associative holds
F $$ ([:X,Y:],f) = F $$ (Y,g)
proof
let D be non empty set ; ::_thesis: for I, J being non empty set
for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) & F is having_a_unity & F is commutative & F is associative holds
F $$ ([:X,Y:],f) = F $$ (Y,g)
let I, J be non empty set ; ::_thesis: for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) & F is having_a_unity & F is commutative & F is associative holds
F $$ ([:X,Y:],f) = F $$ (Y,g)
let F be BinOp of D; ::_thesis: for f being Function of [:I,J:],D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) & F is having_a_unity & F is commutative & F is associative holds
F $$ ([:X,Y:],f) = F $$ (Y,g)
let f be Function of [:I,J:],D; ::_thesis: for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) & F is having_a_unity & F is commutative & F is associative holds
F $$ ([:X,Y:],f) = F $$ (Y,g)
let g be Function of J,D; ::_thesis: for X being Element of Fin I
for Y being Element of Fin J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) & F is having_a_unity & F is commutative & F is associative holds
F $$ ([:X,Y:],f) = F $$ (Y,g)
let X be Element of Fin I; ::_thesis: for Y being Element of Fin J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) & F is having_a_unity & F is commutative & F is associative holds
F $$ ([:X,Y:],f) = F $$ (Y,g)
let Y be Element of Fin J; ::_thesis: ( ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) & F is having_a_unity & F is commutative & F is associative implies F $$ ([:X,Y:],f) = F $$ (Y,g) )
assume that
A1: for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) and
A2: ( F is having_a_unity & F is commutative & F is associative ) ; ::_thesis: F $$ ([:X,Y:],f) = F $$ (Y,g)
defpred S1[ Element of Fin J] means F $$ ([:X,$1:],f) = F $$ ($1,g);
A3: for Y1 being Element of Fin J
for y being Element of J st S1[Y1] holds
S1[Y1 \/ {.y.}]
proof
let Y1 be Element of Fin J; ::_thesis: for y being Element of J st S1[Y1] holds
S1[Y1 \/ {.y.}]
let y be Element of J; ::_thesis: ( S1[Y1] implies S1[Y1 \/ {.y.}] )
assume A4: F $$ ([:X,Y1:],f) = F $$ (Y1,g) ; ::_thesis: S1[Y1 \/ {.y.}]
reconsider s = {.y.} as Element of Fin J ;
percases ( y in Y1 or not y in Y1 ) ;
suppose y in Y1 ; ::_thesis: S1[Y1 \/ {.y.}]
then  Y1 \/ {y} = Y1 by ZFMISC_1:40;
hence  S1[Y1 \/ {.y.}] by A4; ::_thesis: verum
end;
suppose not y in Y1 ; ::_thesis: S1[Y1 \/ {.y.}]
then A5: Y1 misses {y} by ZFMISC_1:50;
then A6: [:X,Y1:] misses [:X,s:] by ZFMISC_1:104;
thus F $$ ([:X,(Y1 \/ {.y.}):],f) = F $$ (([:X,Y1:] \/ [:X,s:]),f) by ZFMISC_1:97
.= F . ((F $$ ([:X,Y1:],f)),(F $$ ([:X,s:],f))) by A2, A6, SETWOP_2:4
.= F . ((F $$ (Y1,g)),(F $$ (s,g))) by A1, A2, A4, Th31
.= F $$ ((Y1 \/ {.y.}),g) by A2, A5, SETWOP_2:4 ; ::_thesis: verum
end;
end;
end;
A7: S1[ {}. J]
proof
reconsider T = {}. [:I,J:] as Element of Fin [:I,J:] ;
 T = [:X,({}. J):] by ZFMISC_1:90;
then  F $$ ([:X,({}. J):],f) = the_unity_wrt F by A2, SETWISEO:31;
hence  S1[ {}. J] by A2, SETWISEO:31; ::_thesis: verum
end;
 for Y1 being Element of Fin J holds S1[Y1] from SETWISEO:sch_4(A7, A3);
hence  F $$ ([:X,Y:],f) = F $$ (Y,g) ; ::_thesis: verum
end;

theorem :: MATRIX_3:33
for K being Field
for A, B, C being Matrix of K st width A = len B & width B = len C holds
(A * B) * C = A * (B * C)
proof
let K be Field; ::_thesis: for A, B, C being Matrix of K st width A = len B & width B = len C holds
(A * B) * C = A * (B * C)
let A, B, C be Matrix of K; ::_thesis: ( width A = len B & width B = len C implies (A * B) * C = A * (B * C) )
assume that
A1: width A = len B and
A2: width B = len C ; ::_thesis: (A * B) * C = A * (B * C)
A3: len (B * C) = width A by A1, A2, Def4;
A4: width (B * C) = width C by A2, Def4;
then A5: width (A * (B * C)) = width C by A3, Def4;
 dom (B * C) = dom B by A1, A3, FINSEQ_3:29;
then A6: Indices (B * C) = [:(dom B),(Seg (width C)):] by A4;
A7: Seg (len B) = dom B by FINSEQ_1:def_3;
A8: len (A * (B * C)) = len A by A3, Def4;
then  dom (A * (B * C)) = dom A by FINSEQ_3:29;
then A9: Indices (A * (B * C)) = [:(dom A),(Seg (width C)):] by A5;
 0. K is_a_unity_wrt the addF of K by FVSUM_1:6;
then A10: the addF of K is having_a_unity by SETWISEO:def_2;
A11: width (A * B) = len C by A1, A2, Def4;
then A12: width ((A * B) * C) = width C by Def4;
A13: len (A * B) = len A by A1, Def4;
then  dom (A * B) = dom A by FINSEQ_3:29;
then A14: Indices (A * B) = [:(dom A),(Seg (width B)):] by A2, A11;
A15: len ((A * B) * C) = len A by A13, A11, Def4;
then A16: dom ((A * B) * C) = dom A by FINSEQ_3:29;
then A17: Indices ((A * B) * C) = [:(dom A),(Seg (width C)):] by A12;
A18: Indices ((A * B) * C) = [:(dom A),(Seg (width C)):] by A12, A16;
now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_((A_*_B)_*_C)_holds_
((A_*_B)_*_C)_*_(i,j)_=_(A_*_(B_*_C))_*_(i,j)
reconsider Y = findom B as Element of Fin NAT ;
reconsider X = findom C as Element of Fin NAT ;
let i, j be Nat; ::_thesis: ( [i,j] in Indices ((A * B) * C) implies ((A * B) * C) * (i,j) = (A * (B * C)) * (i,j) )
deffunc H1( Element of NAT , Element of NAT ) ->  Element of the carrier of K = ((A * (i,$2)) * (B * ($2,$1))) * (C * ($1,j));
consider f being Function of [:NAT,NAT:], the carrier of K such that
A19: for k1, k2 being Element of NAT holds f . (k1,k2) = H1(k1,k2) from BINOP_1:sch_4();
A20: for k being Element of NAT st k in NAT holds
((curry f) . k) | (dom B) = (C * (k,j)) * (mlt ((Line (A,i)),(Col (B,k))))
proof
let k be Element of NAT ; ::_thesis: ( k in NAT implies ((curry f) . k) | (dom B) = (C * (k,j)) * (mlt ((Line (A,i)),(Col (B,k)))) )
assume  k in NAT ; ::_thesis: ((curry f) . k) | (dom B) = (C * (k,j)) * (mlt ((Line (A,i)),(Col (B,k))))
A21: {k} c= NAT by ZFMISC_1:31;
reconsider a = C * (k,j) as Element of K ;
A22: dom (curry f) = NAT by FUNCT_2:def_1;
 dom f = [:NAT,NAT:] by FUNCT_2:def_1;
then A23: dom ((curry f) . k) = proj2 ([:NAT,NAT:] /\ [:{k},(proj2 [:NAT,NAT:]):]) by A22, FUNCT_5:31
.= proj2 ([:{k},NAT:] /\ [:NAT,NAT:]) by FUNCT_5:9
.= proj2 [:{k},NAT:] by A21, ZFMISC_1:101
.= NAT by FUNCT_5:9 ;
then A24: dom (((curry f) . k) | (dom B)) = NAT /\ (dom B) by RELAT_1:61
.= dom B by XBOOLE_1:28 ;
reconsider p = mlt ((Line (A,i)),(Col (B,k))) as FinSequence of K ;
A25: len (mlt ((Line (A,i)),(Col (B,k)))) = len ( the multF of K .: ((Line (A,i)),(Col (B,k)))) by FVSUM_1:def_7;
len (Line (A,i)) = len B by A1, MATRIX_1:def_7
.= len (Col (B,k)) by MATRIX_1:def_8 ;
then A26: len ( the multF of K .: ((Line (A,i)),(Col (B,k)))) = len (Line (A,i)) by FINSEQ_2:72
.= len B by A1, MATRIX_1:def_7 ;
 dom (a multfield) = the carrier of K by FUNCT_2:def_1;
then  ( a * p = (a multfield) * p & rng p c= dom (a multfield) ) by FINSEQ_1:def_4, FVSUM_1:def_6;
then A27: dom (a * p) = dom p by RELAT_1:27;
A28: dom ( the multF of K .: ((Line (A,i)),(Col (B,k)))) = Seg (len ( the multF of K .: ((Line (A,i)),(Col (B,k))))) by FINSEQ_1:def_3;
A29: now__::_thesis:_for_l_being_set_st_l_in_dom_B_holds_
(((curry_f)_._k)_|_(dom_B))_._l_=_((C_*_(k,j))_*_(mlt_((Line_(A,i)),(Col_(B,k)))))_._l
let l be set ; ::_thesis: ( l in dom B implies (((curry f) . k) | (dom B)) . l = ((C * (k,j)) * (mlt ((Line (A,i)),(Col (B,k))))) . l )
assume A30: l in dom B ; ::_thesis: (((curry f) . k) | (dom B)) . l = ((C * (k,j)) * (mlt ((Line (A,i)),(Col (B,k))))) . l
then reconsider l9 = l as Element of NAT ;
A31: l in dom (a * p) by A25, A26, A27, A30, FINSEQ_3:29;
 l9 in dom p by A25, A26, A30, FINSEQ_3:29;
then reconsider b = p . l9 as Element of K by FINSEQ_2:11;
A32: l9 in dom ( the multF of K .: ((Line (A,i)),(Col (B,k)))) by A26, A28, A30, FINSEQ_1:def_3;
thus (((curry f) . k) | (dom B)) . l = ((curry f) . k) . l9 by A30, FUNCT_1:49
.= f . (k,l9) by A22, A23, FUNCT_5:31
.= ((A * (i,l9)) * (B * (l9,k))) * (C * (k,j)) by A19
.= the multF of K . (( the multF of K . (((Line (A,i)) . l9),(B * (l9,k)))),(C * (k,j))) by A1, A7, A30, MATRIX_1:def_7
.= the multF of K . (( the multF of K . (((Line (A,i)) . l9),((Col (B,k)) . l9))),(C * (k,j))) by A30, MATRIX_1:def_8
.= the multF of K . ((( the multF of K .: ((Line (A,i)),(Col (B,k)))) . l9),(C * (k,j))) by A32, FUNCOP_1:22
.= b * a by FVSUM_1:def_7
.= ((C * (k,j)) * (mlt ((Line (A,i)),(Col (B,k))))) . l by A31, FVSUM_1:50 ; ::_thesis: verum
end;
 dom ((C * (k,j)) * (mlt ((Line (A,i)),(Col (B,k))))) = dom B by A25, A26, A27, FINSEQ_3:29;
hence  ((curry f) . k) | (dom B) = (C * (k,j)) * (mlt ((Line (A,i)),(Col (B,k)))) by A24, A29, FUNCT_1:2; ::_thesis: verum
end;
A33: 0. K = the_unity_wrt the addF of K by FVSUM_1:7;
deffunc H2( Element of NAT ) ->  Element of the carrier of K = the addF of K $$ (X,((curry' f) . $1));
deffunc H3( Element of NAT ) ->  Element of the carrier of K = the addF of K $$ (Y,((curry f) . $1));
consider g being Function of NAT, the carrier of K such that
A34: for k being Element of NAT holds g . k = H3(k) from FUNCT_2:sch_4();
A35: dom (g | (dom C)) = (dom g) /\ (dom C) by RELAT_1:61
.= NAT /\ (dom C) by FUNCT_2:def_1
.= dom C by XBOOLE_1:28 ;
len (Line ((A * B),i)) = width (A * B) by MATRIX_1:def_7
.= len C by A1, A2, Def4
.= len (Col (C,j)) by MATRIX_1:def_8 ;
then A36: len ( the multF of K .: ((Line ((A * B),i)),(Col (C,j)))) = len (Col (C,j)) by FINSEQ_2:72
.= len C by MATRIX_1:def_8 ;
assume A37: [i,j] in Indices ((A * B) * C) ; ::_thesis: ((A * B) * C) * (i,j) = (A * (B * C)) * (i,j)
then A38: i in dom A by A17, ZFMISC_1:87;
A39: now__::_thesis:_for_k9_being_set_st_k9_in_dom_C_holds_
(g_|_(dom_C))_._k9_=_(mlt_((Line_((A_*_B),i)),(Col_(C,j))))_._k9
let k9 be set ; ::_thesis: ( k9 in dom C implies (g | (dom C)) . k9 = (mlt ((Line ((A * B),i)),(Col (C,j)))) . k9 )
assume A40: k9 in dom C ; ::_thesis: (g | (dom C)) . k9 = (mlt ((Line ((A * B),i)),(Col (C,j)))) . k9
then reconsider k = k9 as Element of NAT ;
A41: k in dom ( the multF of K .: ((Line ((A * B),i)),(Col (C,j)))) by A36, A40, FINSEQ_3:29;
reconsider p = mlt ((Line (A,i)),(Col (B,k))) as FinSequence of K ;
reconsider a = C * (k,j) as Element of K ;
 dom (a multfield) = the carrier of K by FUNCT_2:def_1;
then  ( a * p = (a multfield) * p & rng p c= dom (a multfield) ) by FINSEQ_1:def_4, FVSUM_1:def_6;
then A42: dom (a * p) = dom p by RELAT_1:27;
len (Line (A,i)) = len B by A1, MATRIX_1:def_7
.= len (Col (B,k)) by MATRIX_1:def_8 ;
then  len ( the multF of K .: ((Line (A,i)),(Col (B,k)))) = len (Line (A,i)) by FINSEQ_2:72
.= len B by A1, MATRIX_1:def_7 ;
then  len B = len p by FVSUM_1:def_7;
then A43: dom ((C * (k,j)) * (mlt ((Line (A,i)),(Col (B,k))))) = dom B by A42, FINSEQ_3:29;
then  ([#] (((C * (k,j)) * (mlt ((Line (A,i)),(Col (B,k))))),(0. K))) | (dom B) = (C * (k,j)) * (mlt ((Line (A,i)),(Col (B,k)))) by SETWOP_2:21;
then A44: ([#] (((C * (k,j)) * (mlt ((Line (A,i)),(Col (B,k))))),(0. K))) | (dom B) = ((curry f) . k) | (dom B) by A20;
 k in Seg (width B) by A2, A40, FINSEQ_1:def_3;
then A45: [i,k] in Indices (A * B) by A14, A38, ZFMISC_1:87;
A46: k in Seg (width (A * B)) by A11, A40, FINSEQ_1:def_3;
thus (g | (dom C)) . k9 = g . k by A35, A40, FUNCT_1:47
.= the addF of K $$ (Y,((curry f) . k)) by A34
.= the addF of K $$ (Y,([#] (((C * (k,j)) * (mlt ((Line (A,i)),(Col (B,k))))),(0. K)))) by A44, FVSUM_1:8, SETWOP_2:7
.= the addF of K $$ (a * p) by A10, A33, A43, SETWOP_2:def_2
.= Sum (a * p) by FVSUM_1:def_8
.= (C * (k,j)) * (Sum (mlt ((Line (A,i)),(Col (B,k))))) by FVSUM_1:73
.= (C * (k,j)) * ((Line (A,i)) "*" (Col (B,k))) by FVSUM_1:def_9
.= ((A * B) * (i,k)) * (C * (k,j)) by A1, A45, Def4
.= the multF of K . (((Line ((A * B),i)) . k),(C * (k,j))) by A46, MATRIX_1:def_7
.= the multF of K . (((Line ((A * B),i)) . k),((Col (C,j)) . k)) by A40, MATRIX_1:def_8
.= ( the multF of K .: ((Line ((A * B),i)),(Col (C,j)))) . k by A41, FUNCOP_1:22
.= (mlt ((Line ((A * B),i)),(Col (C,j)))) . k9 by FVSUM_1:def_7 ; ::_thesis: verum
end;
A47: len ( the multF of K .: ((Line ((A * B),i)),(Col (C,j)))) = len (mlt ((Line ((A * B),i)),(Col (C,j)))) by FVSUM_1:def_7;
then A48: dom C = dom (mlt ((Line ((A * B),i)),(Col (C,j)))) by A36, FINSEQ_3:29;
 dom (mlt ((Line ((A * B),i)),(Col (C,j)))) = dom C by A36, A47, FINSEQ_3:29;
then A49: ([#] ((mlt ((Line ((A * B),i)),(Col (C,j)))),(0. K))) | (dom C) = mlt ((Line ((A * B),i)),(Col (C,j))) by SETWOP_2:21;
len (Col ((B * C),j)) = len (B * C) by MATRIX_1:def_8
.= width A by A1, A2, Def4
.= len (Line (A,i)) by MATRIX_1:def_7 ;
then A50: len ( the multF of K .: ((Line (A,i)),(Col ((B * C),j)))) = len (Line (A,i)) by FINSEQ_2:72
.= width A by MATRIX_1:def_7 ;
A51: len ( the multF of K .: ((Line (A,i)),(Col ((B * C),j)))) = len (mlt ((Line (A,i)),(Col ((B * C),j)))) by FVSUM_1:def_7;
then A52: dom (mlt ((Line (A,i)),(Col ((B * C),j)))) = Y by A1, A50, FINSEQ_3:29;
 dom (mlt ((Line (A,i)),(Col ((B * C),j)))) = dom B by A1, A50, A51, FINSEQ_3:29;
then A53: ([#] ((mlt ((Line (A,i)),(Col ((B * C),j)))),(0. K))) | (dom B) = mlt ((Line (A,i)),(Col ((B * C),j))) by SETWOP_2:21;
consider h being Function of NAT, the carrier of K such that
A54: for k being Element of NAT holds h . k = H2(k) from FUNCT_2:sch_4();
A55: dom (h | (dom B)) = (dom h) /\ (dom B) by RELAT_1:61
.= NAT /\ (dom B) by FUNCT_2:def_1
.= dom B by XBOOLE_1:28 ;
A56: j in Seg (width C) by A17, A37, ZFMISC_1:87;
A57: now__::_thesis:_for_k9_being_set_st_k9_in_dom_B_holds_
(h_|_(dom_B))_._k9_=_(mlt_((Line_(A,i)),(Col_((B_*_C),j))))_._k9
let k9 be set ; ::_thesis: ( k9 in dom B implies (h | (dom B)) . k9 = (mlt ((Line (A,i)),(Col ((B * C),j)))) . k9 )
assume A58: k9 in dom B ; ::_thesis: (h | (dom B)) . k9 = (mlt ((Line (A,i)),(Col ((B * C),j)))) . k9
then reconsider k = k9 as Element of NAT ;
A59: k in Seg (width A) by A1, A58, FINSEQ_1:def_3;
A60: k in dom (B * C) by A1, A3, A58, FINSEQ_3:29;
A61: [k,j] in Indices (B * C) by A6, A56, A58, ZFMISC_1:87;
reconsider p = mlt ((Line (B,k)),(Col (C,j))) as FinSequence of K ;
reconsider a = A * (i,k) as Element of K ;
A62: len (mlt ((Line (B,k)),(Col (C,j)))) = len ( the multF of K .: ((Line (B,k)),(Col (C,j)))) by FVSUM_1:def_7;
 dom f = [:NAT,NAT:] by FUNCT_2:def_1;
then A63: ex G being Function st
( G = (curry' f) . k & dom G = NAT & rng G c= rng f & ( for x being set st x in NAT holds
G . x = f . (x,k) ) ) by FUNCT_5:32;
then A64: dom (((curry' f) . k) | (dom C)) = NAT /\ (dom C) by RELAT_1:61
.= dom C by XBOOLE_1:28 ;
A65: k in dom ( the multF of K .: ((Line (A,i)),(Col ((B * C),j)))) by A1, A50, A58, FINSEQ_3:29;
len (Line (B,k)) = len C by A2, MATRIX_1:def_7
.= len (Col (C,j)) by MATRIX_1:def_8 ;
then A66: len ( the multF of K .: ((Line (B,k)),(Col (C,j)))) = len (Line (B,k)) by FINSEQ_2:72
.= len C by A2, MATRIX_1:def_7 ;
 dom (a multfield) = the carrier of K by FUNCT_2:def_1;
then  ( a * p = (a multfield) * p & rng p c= dom (a multfield) ) by FINSEQ_1:def_4, FVSUM_1:def_6;
then A67: dom (a * p) = dom p by RELAT_1:27;
then A68: dom ((A * (i,k)) * (mlt ((Line (B,k)),(Col (C,j))))) = dom C by A62, A66, FINSEQ_3:29;
A69: now__::_thesis:_for_l_being_set_st_l_in_dom_C_holds_
(((curry'_f)_._k)_|_(dom_C))_._l_=_((A_*_(i,k))_*_(mlt_((Line_(B,k)),(Col_(C,j)))))_._l
let l be set ; ::_thesis: ( l in dom C implies (((curry' f) . k) | (dom C)) . l = ((A * (i,k)) * (mlt ((Line (B,k)),(Col (C,j))))) . l )
assume A70: l in dom C ; ::_thesis: (((curry' f) . k) | (dom C)) . l = ((A * (i,k)) * (mlt ((Line (B,k)),(Col (C,j))))) . l
then reconsider l9 = l as Element of NAT ;
A71: l9 in dom ( the multF of K .: ((Line (B,k)),(Col (C,j)))) by A66, A70, FINSEQ_3:29;
 l9 in dom p by A62, A66, A70, FINSEQ_3:29;
then reconsider b = p . l9 as Element of K by FINSEQ_2:11;
A72: l9 in Seg (width B) by A2, A70, FINSEQ_1:def_3;
A73: l in dom (a * p) by A62, A66, A67, A70, FINSEQ_3:29;
thus (((curry' f) . k) | (dom C)) . l = ((curry' f) . k) . l9 by A70, FUNCT_1:49
.= f . (l9,k) by A63
.= ((A * (i,k)) * (B * (k,l9))) * (C * (l9,j)) by A19
.= (A * (i,k)) * ((B * (k,l9)) * (C * (l9,j))) by GROUP_1:def_3
.= the multF of K . ((A * (i,k)),( the multF of K . (((Line (B,k)) . l9),(C * (l9,j))))) by A72, MATRIX_1:def_7
.= the multF of K . ((A * (i,k)),( the multF of K . (((Line (B,k)) . l9),((Col (C,j)) . l9)))) by A70, MATRIX_1:def_8
.= the multF of K . ((A * (i,k)),(( the multF of K .: ((Line (B,k)),(Col (C,j)))) . l9)) by A71, FUNCOP_1:22
.= a * b by FVSUM_1:def_7
.= ((A * (i,k)) * (mlt ((Line (B,k)),(Col (C,j))))) . l by A73, FVSUM_1:50 ; ::_thesis: verum
end;
 ([#] (((A * (i,k)) * (mlt ((Line (B,k)),(Col (C,j))))),(0. K))) | (dom C) = (A * (i,k)) * (mlt ((Line (B,k)),(Col (C,j)))) by A68, SETWOP_2:21;
then A74: ([#] (((A * (i,k)) * (mlt ((Line (B,k)),(Col (C,j))))),(0. K))) | (dom C) = ((curry' f) . k) | (dom C) by A64, A68, A69, FUNCT_1:2;
thus (h | (dom B)) . k9 = h . k by A55, A58, FUNCT_1:47
.= the addF of K $$ (X,((curry' f) . k)) by A54
.= the addF of K $$ (X,([#] (((A * (i,k)) * (mlt ((Line (B,k)),(Col (C,j))))),(0. K)))) by A74, FVSUM_1:8, SETWOP_2:7
.= the addF of K $$ (a * p) by A10, A33, A68, SETWOP_2:def_2
.= Sum (a * p) by FVSUM_1:def_8
.= (A * (i,k)) * (Sum (mlt ((Line (B,k)),(Col (C,j))))) by FVSUM_1:73
.= (A * (i,k)) * ((Line (B,k)) "*" (Col (C,j))) by FVSUM_1:def_9
.= (A * (i,k)) * ((B * C) * (k,j)) by A2, A61, Def4
.= the multF of K . (((Line (A,i)) . k),((B * C) * (k,j))) by A59, MATRIX_1:def_7
.= the multF of K . (((Line (A,i)) . k),((Col ((B * C),j)) . k)) by A60, MATRIX_1:def_8
.= ( the multF of K .: ((Line (A,i)),(Col ((B * C),j)))) . k by A65, FUNCOP_1:22
.= (mlt ((Line (A,i)),(Col ((B * C),j)))) . k9 by FVSUM_1:def_7 ; ::_thesis: verum
end;
 dom (mlt ((Line (A,i)),(Col ((B * C),j)))) = dom B by A1, A50, A51, FINSEQ_3:29;
then A75: h | (dom B) = mlt ((Line (A,i)),(Col ((B * C),j))) by A55, A57, FUNCT_1:2;
 dom (mlt ((Line ((A * B),i)),(Col (C,j)))) = dom C by A36, A47, FINSEQ_3:29;
then A76: g | (dom C) = mlt ((Line ((A * B),i)),(Col (C,j))) by A35, A39, FUNCT_1:2;
thus ((A * B) * C) * (i,j) = (Line ((A * B),i)) "*" (Col (C,j)) by A11, A37, Def4
.= Sum (mlt ((Line ((A * B),i)),(Col (C,j)))) by FVSUM_1:def_9
.= the addF of K $$ (mlt ((Line ((A * B),i)),(Col (C,j)))) by FVSUM_1:def_8
.= the addF of K $$ ((findom C),([#] ((mlt ((Line ((A * B),i)),(Col (C,j)))),(0. K)))) by A10, A33, A48, SETWOP_2:def_2
.= the addF of K $$ (X,g) by A10, A49, A76, SETWOP_2:7
.= the addF of K $$ ([:X,Y:],f) by A10, A34, Th30
.= the addF of K $$ (Y,h) by A10, A54, Th32
.= the addF of K $$ ((findom (mlt ((Line (A,i)),(Col ((B * C),j))))),([#] ((mlt ((Line (A,i)),(Col ((B * C),j)))),(the_unity_wrt the addF of K)))) by A10, A33, A53, A75, A52, SETWOP_2:7
.= the addF of K $$ (mlt ((Line (A,i)),(Col ((B * C),j)))) by A10, SETWOP_2:def_2
.= Sum (mlt ((Line (A,i)),(Col ((B * C),j)))) by FVSUM_1:def_8
.= (Line (A,i)) "*" (Col ((B * C),j)) by FVSUM_1:def_9
.= (A * (B * C)) * (i,j) by A3, A9, A18, A37, Def4 ; ::_thesis: verum
end;
hence  (A * B) * C = A * (B * C) by A8, A5, A15, A12, MATRIX_1:21; ::_thesis: verum
end;

begin

definition
let n be Nat;
let K be Field;
let M be Matrix of n,K;
let p be Element of Permutations n;
func Path_matrix (p,M) ->  FinSequence of K means :Def7: :: MATRIX_3:def 7
( len it = n & ( for i, j being Nat st i in dom it & j = p . i holds
it . i = M * (i,j) ) );
existence
 ex b1 being FinSequence of K st
( len b1 = n & ( for i, j being Nat st i in dom b1 & j = p . i holds
b1 . i = M * (i,j) ) )
proof
defpred S1[ Nat, set ] means  for j being Nat st j = p . $1 holds
$2 = M * ($1,j);
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
A1: for k being Nat st k in Seg n1 holds
ex x being Element of K st S1[k,x]
proof
reconsider p = p as Function of (Seg n),(Seg n) by MATRIX_2:def_9;
let k be Nat; ::_thesis: ( k in Seg n1 implies ex x being Element of K st S1[k,x] )
assume  k in Seg n1 ; ::_thesis: ex x being Element of K st S1[k,x]
then  p . k in Seg n by FUNCT_2:5;
then reconsider j = p . k as Element of NAT ;
reconsider x = M * (k,j) as Element of K ;
take  x ; ::_thesis: S1[k,x]
thus  S1[k,x] ; ::_thesis: verum
end;
consider t being FinSequence of K such that
A2: dom t = Seg n1 and
A3: for k being Nat st k in Seg n1 holds
S1[k,t . k] from FINSEQ_1:sch_5(A1);
take  t ; ::_thesis: ( len t = n & ( for i, j being Nat st i in dom t & j = p . i holds
t . i = M * (i,j) ) )
thus  len t = n by A2, FINSEQ_1:def_3; ::_thesis: for i, j being Nat st i in dom t & j = p . i holds
t . i = M * (i,j)
let i, j be Nat; ::_thesis: ( i in dom t & j = p . i implies t . i = M * (i,j) )
assume  ( i in dom t & j = p . i ) ; ::_thesis: t . i = M * (i,j)
hence  t . i = M * (i,j) by A2, A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being FinSequence of K st len b1 = n & ( for i, j being Nat st i in dom b1 & j = p . i holds
b1 . i = M * (i,j) ) & len b2 = n & ( for i, j being Nat st i in dom b2 & j = p . i holds
b2 . i = M * (i,j) ) holds
b1 = b2
proof
 for p1, p2 being FinSequence of K st len p1 = n & ( for i, j being Nat st i in dom p1 & j = p . i holds
p1 . i = M * (i,j) ) & len p2 = n & ( for i, j being Nat st i in dom p2 & j = p . i holds
p2 . i = M * (i,j) ) holds
p1 = p2
proof
let p1, p2 be FinSequence of K; ::_thesis: ( len p1 = n & ( for i, j being Nat st i in dom p1 & j = p . i holds
p1 . i = M * (i,j) ) & len p2 = n & ( for i, j being Nat st i in dom p2 & j = p . i holds
p2 . i = M * (i,j) ) implies p1 = p2 )
assume that
A4: len p1 = n and
A5: for i, j being Nat st i in dom p1 & j = p . i holds
p1 . i = M * (i,j) and
A6: len p2 = n and
A7: for i, j being Nat st i in dom p2 & j = p . i holds
p2 . i = M * (i,j) ; ::_thesis: p1 = p2
A8: dom p2 = Seg n by A6, FINSEQ_1:def_3;
A9: dom p1 = Seg n by A4, FINSEQ_1:def_3;
 for i being Nat st i in Seg n holds
p1 . i = p2 . i
proof
reconsider p = p as Function of (Seg n),(Seg n) by MATRIX_2:def_9;
let i be Nat; ::_thesis: ( i in Seg n implies p1 . i = p2 . i )
assume A10: i in Seg n ; ::_thesis: p1 . i = p2 . i
then  p . i in Seg n by FUNCT_2:5;
then reconsider j = p . i as Element of NAT ;
 p1 . i = M * (i,j) by A5, A9, A10;
hence  p1 . i = p2 . i by A7, A8, A10; ::_thesis: verum
end;
hence  p1 = p2 by A9, A8, FINSEQ_1:13; ::_thesis: verum
end;
hence  for b1, b2 being FinSequence of K st len b1 = n & ( for i, j being Nat st i in dom b1 & j = p . i holds
b1 . i = M * (i,j) ) & len b2 = n & ( for i, j being Nat st i in dom b2 & j = p . i holds
b2 . i = M * (i,j) ) holds
b1 = b2 ; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines Path_matrix MATRIX_3:def_7_:_
 for n being Nat
for K being Field
for M being Matrix of n,K
for p being Element of Permutations n
for b5 being FinSequence of K holds
( b5 = Path_matrix (p,M) iff ( len b5 = n & ( for i, j being Nat st i in dom b5 & j = p . i holds
b5 . i = M * (i,j) ) ) );

definition
let n be Nat;
let K be Field;
let M be Matrix of n,K;
func Path_product M ->  Function of (Permutations n), the carrier of K means :Def8: :: MATRIX_3:def 8
 for p being Element of Permutations n holds it . p = - (( the multF of K $$ (Path_matrix (p,M))),p);
existence
 ex b1 being Function of (Permutations n), the carrier of K st
for p being Element of Permutations n holds b1 . p = - (( the multF of K $$ (Path_matrix (p,M))),p)
proof
deffunc H1( Element of Permutations n) ->  Element of the carrier of K = - (( the multF of K $$ (Path_matrix ($1,M))),$1);
consider f being Function of (Permutations n), the carrier of K such that
A1: for p being Element of Permutations n holds f . p = H1(p) from FUNCT_2:sch_4();
take  f ; ::_thesis: for p being Element of Permutations n holds f . p = - (( the multF of K $$ (Path_matrix (p,M))),p)
thus  for p being Element of Permutations n holds f . p = - (( the multF of K $$ (Path_matrix (p,M))),p) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (Permutations n), the carrier of K st ( for p being Element of Permutations n holds b1 . p = - (( the multF of K $$ (Path_matrix (p,M))),p) ) & ( for p being Element of Permutations n holds b2 . p = - (( the multF of K $$ (Path_matrix (p,M))),p) ) holds
b1 = b2
proof
let f1, f2 be Function of (Permutations n), the carrier of K; ::_thesis: ( ( for p being Element of Permutations n holds f1 . p = - (( the multF of K $$ (Path_matrix (p,M))),p) ) & ( for p being Element of Permutations n holds f2 . p = - (( the multF of K $$ (Path_matrix (p,M))),p) ) implies f1 = f2 )
assume that
A2: for p being Element of Permutations n holds f1 . p = - (( the multF of K $$ (Path_matrix (p,M))),p) and
A3: for p being Element of Permutations n holds f2 . p = - (( the multF of K $$ (Path_matrix (p,M))),p) ; ::_thesis: f1 = f2
now__::_thesis:_for_p_being_Element_of_Permutations_n_holds_f1_._p_=_f2_._p
let p be Element of Permutations n; ::_thesis: f1 . p = f2 . p
 f1 . p = - (( the multF of K $$ (Path_matrix (p,M))),p) by A2;
hence  f1 . p = f2 . p by A3; ::_thesis: verum
end;
hence  f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines Path_product MATRIX_3:def_8_:_
 for n being Nat
for K being Field
for M being Matrix of n,K
for b4 being Function of (Permutations n), the carrier of K holds
( b4 = Path_product M iff for p being Element of Permutations n holds b4 . p = - (( the multF of K $$ (Path_matrix (p,M))),p) );

definition
let n be Nat;
let K be Field;
let M be Matrix of n,K;
func Det M ->  Element of K equals :: MATRIX_3:def 9
 the addF of K $$ ((FinOmega (Permutations n)),(Path_product M));
coherence
 the addF of K $$ ((FinOmega (Permutations n)),(Path_product M)) is Element of K ;
end;

:: deftheorem  defines Det MATRIX_3:def_9_:_
 for n being Nat
for K being Field
for M being Matrix of n,K holds Det M = the addF of K $$ ((FinOmega (Permutations n)),(Path_product M));

theorem :: MATRIX_3:34
for K being Field
for a being Element of K holds Det <*<*a*>*> = a
proof
let K be Field; ::_thesis: for a being Element of K holds Det <*<*a*>*> = a
let a be Element of K; ::_thesis: Det <*<*a*>*> = a
set M = <*<*a*>*>;
A1: (Path_product <*<*a*>*>) . (idseq 1) = a
proof
reconsider p = idseq 1 as Element of Permutations 1 by MATRIX_2:def_9;
A2: - (a,p) = a
proof
reconsider q = id (Seg 1) as Element of Permutations 1 by MATRIX_2:def_9;
 len (Permutations 1) = 1 by MATRIX_2:18;
then  q is even by MATRIX_2:25;
hence  - (a,p) = a by MATRIX_2:def_13; ::_thesis: verum
end;
A3: len (Path_matrix (p,<*<*a*>*>)) = 1 by Def7;
then A4: dom (Path_matrix (p,<*<*a*>*>)) = Seg 1 by FINSEQ_1:def_3;
then A5: 1 in dom (Path_matrix (p,<*<*a*>*>)) by FINSEQ_1:2, TARSKI:def_1;
then  1 = p . 1 by A4, FUNCT_1:18;
then  (Path_matrix (p,<*<*a*>*>)) . 1 = <*<*a*>*> * (1,1) by A5, Def7;
then  (Path_matrix (p,<*<*a*>*>)) . 1 = a by MATRIX_2:5;
then A6: Path_matrix (p,<*<*a*>*>) = <*a*> by A3, FINSEQ_1:40;
 ( (Path_product <*<*a*>*>) . p = - (( the multF of K $$ (Path_matrix (p,<*<*a*>*>))),p) & <*a*> = 1 |-> a ) by Def8, FINSEQ_2:59;
hence  (Path_product <*<*a*>*>) . (idseq 1) = a by A6, A2, FINSOP_1:16; ::_thesis: verum
end;
 ( FinOmega (Permutations 1) = {(idseq 1)} & idseq 1 in Permutations 1 ) by MATRIX_2:19, MATRIX_2:def_14, TARSKI:def_1;
hence  Det <*<*a*>*> = a by A1, SETWISEO:17; ::_thesis: verum
end;

definition
let n be Nat;
let K be Field;
let M be Matrix of n,K;
func diagonal_of_Matrix M ->  FinSequence of K means :: MATRIX_3:def 10
( len it = n & ( for i being Nat st i in Seg n holds
it . i = M * (i,i) ) );
existence
 ex b1 being FinSequence of K st
( len b1 = n & ( for i being Nat st i in Seg n holds
b1 . i = M * (i,i) ) )
proof
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
deffunc H1( Nat) ->  Element of the carrier of K = M * ($1,$1);
consider z being FinSequence of K such that
A1: ( len z = n1 & ( for i being Nat st i in dom z holds
z . i = H1(i) ) ) from FINSEQ_2:sch_1();
take  z ; ::_thesis: ( len z = n & ( for i being Nat st i in Seg n holds
z . i = M * (i,i) ) )
 dom z = Seg n1 by A1, FINSEQ_1:def_3;
hence  ( len z = n & ( for i being Nat st i in Seg n holds
z . i = M * (i,i) ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being FinSequence of K st len b1 = n & ( for i being Nat st i in Seg n holds
b1 . i = M * (i,i) ) & len b2 = n & ( for i being Nat st i in Seg n holds
b2 . i = M * (i,i) ) holds
b1 = b2
proof
let p1, p2 be FinSequence of K; ::_thesis: ( len p1 = n & ( for i being Nat st i in Seg n holds
p1 . i = M * (i,i) ) & len p2 = n & ( for i being Nat st i in Seg n holds
p2 . i = M * (i,i) ) implies p1 = p2 )
assume that
A2: len p1 = n and
A3: for i being Nat st i in Seg n holds
p1 . i = M * (i,i) and
A4: len p2 = n and
A5: for i being Nat st i in Seg n holds
p2 . i = M * (i,i) ; ::_thesis: p1 = p2
A6: now__::_thesis:_for_i_being_Nat_st_i_in_Seg_n_holds_
p1_._i_=_p2_._i
let i be Nat; ::_thesis: ( i in Seg n implies p1 . i = p2 . i )
assume A7: i in Seg n ; ::_thesis: p1 . i = p2 . i
then  p1 . i = M * (i,i) by A3;
hence  p1 . i = p2 . i by A5, A7; ::_thesis: verum
end;
 ( dom p1 = Seg n & dom p2 = Seg n ) by A2, A4, FINSEQ_1:def_3;
hence  p1 = p2 by A6, FINSEQ_1:13; ::_thesis: verum
end;
end;

:: deftheorem  defines diagonal_of_Matrix MATRIX_3:def_10_:_
 for n being Nat
for K being Field
for M being Matrix of n,K
for b4 being FinSequence of K holds
( b4 = diagonal_of_Matrix M iff ( len b4 = n & ( for i being Nat st i in Seg n holds
b4 . i = M * (i,i) ) ) );