:: Some Properties of Line and Column Operations on Matrices
:: by Xiquan Liang , Tao Sun and Dahai Hu
::
:: Received August 13, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users


begin

Lm1:  for m, n being Nat
for K being Field
for k, l being Nat
for M, M1, M2 being Matrix of n,m,K
for pK, qK being FinSequence of K
for i, j being Nat st i in Seg n & j in Seg (width M) & pK = Line (M,l) & qK = Line (M,k) & M1 = RLine (M,k,pK) & M2 = RLine (M1,l,qK) holds
( ( i = l implies M2 * (i,j) = M * (k,j) ) &amp; ( i = k implies M2 * (i,j) = M * (l,j) ) &amp; ( i <> l &amp; i <> k implies M2 * (i,j) = M * (i,j) ) )
proofend;

definition
let n, m be Nat;
let K be Field;
let M be Matrix of n,m,K;
let l, k be Nat;
func InterchangeLine (M,l,k) ->  Matrix of n,m,K means :Def1: :: MATRIX12:def 1
( len it = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( i = l implies it * (i,j) = M * (k,j) ) &amp; ( i = k implies it * (i,j) = M * (l,j) ) &amp; ( i <> l &amp; i <> k implies it * (i,j) = M * (i,j) ) ) ) );
existence
 ex b1 being Matrix of n,m,K st
( len b1 = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( i = l implies b1 * (i,j) = M * (k,j) ) &amp; ( i = k implies b1 * (i,j) = M * (l,j) ) &amp; ( i <> l &amp; i <> k implies b1 * (i,j) = M * (i,j) ) ) ) )
proofend;
uniqueness
 for b1, b2 being Matrix of n,m,K st len b1 = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( i = l implies b1 * (i,j) = M * (k,j) ) &amp; ( i = k implies b1 * (i,j) = M * (l,j) ) &amp; ( i <> l &amp; i <> k implies b1 * (i,j) = M * (i,j) ) ) ) &amp; len b2 = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( i = l implies b2 * (i,j) = M * (k,j) ) &amp; ( i = k implies b2 * (i,j) = M * (l,j) ) &amp; ( i <> l &amp; i <> k implies b2 * (i,j) = M * (i,j) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines InterchangeLine MATRIX12:def_1_:_
 for n, m being Nat
for K being Field
for M being Matrix of n,m,K
for l, k being Nat
for b7 being Matrix of n,m,K holds
( b7 = InterchangeLine (M,l,k) iff ( len b7 = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( i = l implies b7 * (i,j) = M * (k,j) ) &amp; ( i = k implies b7 * (i,j) = M * (l,j) ) &amp; ( i <> l &amp; i <> k implies b7 * (i,j) = M * (i,j) ) ) ) ) );

theorem Th1: :: MATRIX12:1
for n, m being Nat
for K being Field
for M1, M2 being Matrix of n,m,K holds width M1 = width M2
proofend;

theorem Th2: :: MATRIX12:2
for m, n, l, k being Nat
for K being Field
for M, M1 being Matrix of n,m,K
for i being Nat st l in dom M &amp; k in dom M &amp; i in dom M &amp; M1 = InterchangeLine (M,l,k) holds
( ( i = l implies Line (M1,i) = Line (M,k) ) &amp; ( i = k implies Line (M1,i) = Line (M,l) ) &amp; ( i <> l &amp; i <> k implies Line (M1,i) = Line (M,i) ) )
proofend;

theorem Th3: :: MATRIX12:3
for m, n being Nat
for K being Field
for a being Element of K
for i, j being Nat
for M being Matrix of n,m,K st i in dom M &amp; j in Seg (width M) holds
(a * (Line (M,i))) . j = a * (M * (i,j))
proofend;

Lm2:  for m, n being Nat
for K being Field
for a being Element of K
for l being Nat
for M, M1 being Matrix of n,m,K
for pK being FinSequence of K
for i, j being Nat st i in Seg n &amp; j in Seg (width M) &amp; pK = Line (M,l) &amp; M1 = RLine (M,l,(a * pK)) holds
( ( i = l implies M1 * (i,j) = a * (M * (l,j)) ) &amp; ( i <> l implies M1 * (i,j) = M * (i,j) ) )
proofend;

definition
let n, m be Nat;
let K be Field;
let M be Matrix of n,m,K;
let l be Nat;
let a be Element of K;
func ScalarXLine (M,l,a) ->  Matrix of n,m,K means :Def2: :: MATRIX12:def 2
( len it = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( i = l implies it * (i,j) = a * (M * (l,j)) ) &amp; ( i <> l implies it * (i,j) = M * (i,j) ) ) ) );
existence
 ex b1 being Matrix of n,m,K st
( len b1 = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( i = l implies b1 * (i,j) = a * (M * (l,j)) ) &amp; ( i <> l implies b1 * (i,j) = M * (i,j) ) ) ) )
proofend;
uniqueness
 for b1, b2 being Matrix of n,m,K st len b1 = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( i = l implies b1 * (i,j) = a * (M * (l,j)) ) &amp; ( i <> l implies b1 * (i,j) = M * (i,j) ) ) ) &amp; len b2 = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( i = l implies b2 * (i,j) = a * (M * (l,j)) ) &amp; ( i <> l implies b2 * (i,j) = M * (i,j) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines ScalarXLine MATRIX12:def_2_:_
 for n, m being Nat
for K being Field
for M being Matrix of n,m,K
for l being Nat
for a being Element of K
for b7 being Matrix of n,m,K holds
( b7 = ScalarXLine (M,l,a) iff ( len b7 = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( i = l implies b7 * (i,j) = a * (M * (l,j)) ) &amp; ( i <> l implies b7 * (i,j) = M * (i,j) ) ) ) ) );

theorem Th4: :: MATRIX12:4
for n, m, l, i being Nat
for K being Field
for a being Element of K
for M, M1 being Matrix of n,m,K st l in dom M &amp; i in dom M &amp; M1 = ScalarXLine (M,l,a) holds
( ( i = l implies Line (M1,i) = a * (Line (M,l)) ) &amp; ( i <> l implies Line (M1,i) = Line (M,i) ) )
proofend;

Lm3:  for m, i, n, j, k, l being Nat
for K being Field
for a being Element of K
for M, M1 being Matrix of n,m,K
for pK, qK being FinSequence of K st i in Seg n &amp; j in Seg (width M) &amp; k in dom M &amp; pK = Line (M,l) &amp; qK = Line (M,k) &amp; M1 = RLine (M,l,((a * qK) + pK)) holds
( ( i = l implies M1 * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) &amp; ( i <> l implies M1 * (i,j) = M * (i,j) ) )
proofend;

definition
let n, m be Nat;
let K be Field;
let M be Matrix of n,m,K;
let l, k be Nat;
let a be Element of K;
assume A1: k in dom M ;
func RlineXScalar (M,l,k,a) ->  Matrix of n,m,K means :Def3: :: MATRIX12:def 3
( len it = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( i = l implies it * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) &amp; ( i <> l implies it * (i,j) = M * (i,j) ) ) ) );
existence
 ex b1 being Matrix of n,m,K st
( len b1 = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( i = l implies b1 * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) &amp; ( i <> l implies b1 * (i,j) = M * (i,j) ) ) ) )
proofend;
uniqueness
 for b1, b2 being Matrix of n,m,K st len b1 = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( i = l implies b1 * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) &amp; ( i <> l implies b1 * (i,j) = M * (i,j) ) ) ) &amp; len b2 = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( i = l implies b2 * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) &amp; ( i <> l implies b2 * (i,j) = M * (i,j) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines RlineXScalar MATRIX12:def_3_:_
 for n, m being Nat
for K being Field
for M being Matrix of n,m,K
for l, k being Nat
for a being Element of K st k in dom M holds
for b8 being Matrix of n,m,K holds
( b8 = RlineXScalar (M,l,k,a) iff ( len b8 = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( i = l implies b8 * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) &amp; ( i <> l implies b8 * (i,j) = M * (i,j) ) ) ) ) );

theorem Th5: :: MATRIX12:5
for n, m, l, k, i being Nat
for K being Field
for a being Element of K
for M, M1 being Matrix of n,m,K st l in dom M &amp; k in dom M &amp; i in dom M &amp; M1 = RlineXScalar (M,l,k,a) holds
( ( i = l implies Line (M1,i) = (a * (Line (M,k))) + (Line (M,l)) ) &amp; ( i <> l implies Line (M1,i) = Line (M,i) ) )
proofend;

notation
let n, m be Nat;
let K be Field;
let M be Matrix of n,m,K;
let l, k be Nat;
synonym  ILine (M,l,k) for  InterchangeLine (M,l,k);
end;

notation
let n, m be Nat;
let K be Field;
let M be Matrix of n,m,K;
let l be Nat;
let a be Element of K;
synonym  SXLine (M,l,a) for  ScalarXLine (M,l,a);
end;

notation
let n, m be Nat;
let K be Field;
let M be Matrix of n,m,K;
let l, k be Nat;
let a be Element of K;
synonym  RLineXS (M,l,k,a) for  RlineXScalar (M,l,k,a);
end;

theorem Th6: :: MATRIX12:6
for l, n, k being Nat
for K being Field
for A being Matrix of n,K st l in dom (1. (K,n)) &amp; k in dom (1. (K,n)) holds
(ILine ((1. (K,n)),l,k)) * A = ILine (A,l,k)
proofend;

theorem Th7: :: MATRIX12:7
for n being Nat
for K being Field
for l being Nat
for a being Element of K
for A being Matrix of n,K st l in dom (1. (K,n)) holds
(SXLine ((1. (K,n)),l,a)) * A = SXLine (A,l,a)
proofend;

theorem Th8: :: MATRIX12:8
for l, n, k being Nat
for K being Field
for a being Element of K
for A being Matrix of n,K st l in dom (1. (K,n)) &amp; k in dom (1. (K,n)) holds
(RLineXS ((1. (K,n)),l,k,a)) * A = RLineXS (A,l,k,a)
proofend;

theorem :: MATRIX12:9
for n, m, k being Nat
for K being Field
for M being Matrix of n,m,K holds ILine (M,k,k) = M
proofend;

theorem :: MATRIX12:10
for n, m, l, k being Nat
for K being Field
for M being Matrix of n,m,K holds ILine (M,l,k) = ILine (M,k,l)
proofend;

theorem Th11: :: MATRIX12:11
for n, m, l, k being Nat
for K being Field
for M being Matrix of n,m,K st l in dom M &amp; k in dom M holds
ILine ((ILine (M,l,k)),l,k) = M
proofend;

theorem Th12: :: MATRIX12:12
for l, n, k being Nat
for K being Field st l in dom (1. (K,n)) &amp; k in dom (1. (K,n)) holds
( ILine ((1. (K,n)),l,k) is invertible &amp; (ILine ((1. (K,n)),l,k)) ~ = ILine ((1. (K,n)),l,k) )
proofend;

Lm4:  for n being Nat
for K being Field
for i, j, l, k being Nat
for a being Element of K st [i,j] in Indices (1. (K,n)) &amp; l in dom (1. (K,n)) &amp; k in dom (1. (K,n)) &amp; k <> l holds
(1. (K,n)) * (i,j) = (RLineXS ((RLineXS ((1. (K,n)),l,k,(- a))),l,k,a)) * (i,j)
proofend;

theorem Th13: :: MATRIX12:13
for l, n, k being Nat
for K being Field
for a being Element of K st l in dom (1. (K,n)) &amp; k in dom (1. (K,n)) &amp; k <> l holds
( RLineXS ((1. (K,n)),l,k,a) is invertible &amp; (RLineXS ((1. (K,n)),l,k,a)) ~ = RLineXS ((1. (K,n)),l,k,(- a)) )
proofend;

theorem Th14: :: MATRIX12:14
for l, n being Nat
for K being Field
for a being Element of K st l in dom (1. (K,n)) &amp; a <> 0. K holds
( SXLine ((1. (K,n)),l,a) is invertible &amp; (SXLine ((1. (K,n)),l,a)) ~ = SXLine ((1. (K,n)),l,(a ")) )
proofend;

definition
let n, m be Nat;
let K be Field;
let M be Matrix of n,m,K;
let l, k be Nat;
assume that
A1: l in Seg (width M) and
A2: k in Seg (width M) and
A3: n > 0 and
A4: m > 0 ;
func InterchangeCol (M,l,k) ->  Matrix of n,m,K means :Def4: :: MATRIX12:def 4
( len it = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( j = l implies it * (i,j) = M * (i,k) ) &amp; ( j = k implies it * (i,j) = M * (i,l) ) &amp; ( j <> l &amp; j <> k implies it * (i,j) = M * (i,j) ) ) ) );
existence
 ex b1 being Matrix of n,m,K st
( len b1 = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( j = l implies b1 * (i,j) = M * (i,k) ) &amp; ( j = k implies b1 * (i,j) = M * (i,l) ) &amp; ( j <> l &amp; j <> k implies b1 * (i,j) = M * (i,j) ) ) ) )
proofend;
uniqueness
 for b1, b2 being Matrix of n,m,K st len b1 = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( j = l implies b1 * (i,j) = M * (i,k) ) &amp; ( j = k implies b1 * (i,j) = M * (i,l) ) &amp; ( j <> l &amp; j <> k implies b1 * (i,j) = M * (i,j) ) ) ) &amp; len b2 = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( j = l implies b2 * (i,j) = M * (i,k) ) &amp; ( j = k implies b2 * (i,j) = M * (i,l) ) &amp; ( j <> l &amp; j <> k implies b2 * (i,j) = M * (i,j) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines InterchangeCol MATRIX12:def_4_:_
 for n, m being Nat
for K being Field
for M being Matrix of n,m,K
for l, k being Nat st l in Seg (width M) &amp; k in Seg (width M) &amp; n > 0 &amp; m > 0 holds
for b7 being Matrix of n,m,K holds
( b7 = InterchangeCol (M,l,k) iff ( len b7 = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( j = l implies b7 * (i,j) = M * (i,k) ) &amp; ( j = k implies b7 * (i,j) = M * (i,l) ) &amp; ( j <> l &amp; j <> k implies b7 * (i,j) = M * (i,j) ) ) ) ) );

definition
let n, m be Nat;
let K be Field;
let M be Matrix of n,m,K;
let l be Nat;
let a be Element of K;
assume that
A1: l in Seg (width M) and
A2: n > 0 and
A3: m > 0 ;
func ScalarXCol (M,l,a) ->  Matrix of n,m,K means :Def5: :: MATRIX12:def 5
( len it = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( j = l implies it * (i,j) = a * (M * (i,l)) ) &amp; ( j <> l implies it * (i,j) = M * (i,j) ) ) ) );
existence
 ex b1 being Matrix of n,m,K st
( len b1 = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( j = l implies b1 * (i,j) = a * (M * (i,l)) ) &amp; ( j <> l implies b1 * (i,j) = M * (i,j) ) ) ) )
proofend;
uniqueness
 for b1, b2 being Matrix of n,m,K st len b1 = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( j = l implies b1 * (i,j) = a * (M * (i,l)) ) &amp; ( j <> l implies b1 * (i,j) = M * (i,j) ) ) ) &amp; len b2 = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( j = l implies b2 * (i,j) = a * (M * (i,l)) ) &amp; ( j <> l implies b2 * (i,j) = M * (i,j) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines ScalarXCol MATRIX12:def_5_:_
 for n, m being Nat
for K being Field
for M being Matrix of n,m,K
for l being Nat
for a being Element of K st l in Seg (width M) &amp; n > 0 &amp; m > 0 holds
for b7 being Matrix of n,m,K holds
( b7 = ScalarXCol (M,l,a) iff ( len b7 = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( j = l implies b7 * (i,j) = a * (M * (i,l)) ) &amp; ( j <> l implies b7 * (i,j) = M * (i,j) ) ) ) ) );

definition
let n, m be Nat;
let K be Field;
let M be Matrix of n,m,K;
let l, k be Nat;
let a be Element of K;
assume that
A1: l in Seg (width M) and
A2: k in Seg (width M) and
A3: n > 0 and
A4: m > 0 ;
func RcolXScalar (M,l,k,a) ->  Matrix of n,m,K means :Def6: :: MATRIX12:def 6
( len it = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( j = l implies it * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) &amp; ( j <> l implies it * (i,j) = M * (i,j) ) ) ) );
existence
 ex b1 being Matrix of n,m,K st
( len b1 = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( j = l implies b1 * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) &amp; ( j <> l implies b1 * (i,j) = M * (i,j) ) ) ) )
proofend;
uniqueness
 for b1, b2 being Matrix of n,m,K st len b1 = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( j = l implies b1 * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) &amp; ( j <> l implies b1 * (i,j) = M * (i,j) ) ) ) &amp; len b2 = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( j = l implies b2 * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) &amp; ( j <> l implies b2 * (i,j) = M * (i,j) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines RcolXScalar MATRIX12:def_6_:_
 for n, m being Nat
for K being Field
for M being Matrix of n,m,K
for l, k being Nat
for a being Element of K st l in Seg (width M) &amp; k in Seg (width M) &amp; n > 0 &amp; m > 0 holds
for b8 being Matrix of n,m,K holds
( b8 = RcolXScalar (M,l,k,a) iff ( len b8 = len M &amp; ( for i, j being Nat st i in dom M &amp; j in Seg (width M) holds
( ( j = l implies b8 * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) &amp; ( j <> l implies b8 * (i,j) = M * (i,j) ) ) ) ) );

notation
let n, m be Nat;
let K be Field;
let M be Matrix of n,m,K;
let l, k be Nat;
synonym  ICol (M,l,k) for  InterchangeCol (M,l,k);
end;

notation
let n, m be Nat;
let K be Field;
let M be Matrix of n,m,K;
let l be Nat;
let a be Element of K;
synonym  SXCol (M,l,a) for  ScalarXCol (M,l,a);
end;

notation
let n, m be Nat;
let K be Field;
let M be Matrix of n,m,K;
let l, k be Nat;
let a be Element of K;
synonym  RColXS (M,l,k,a) for  RcolXScalar (M,l,k,a);
end;

theorem Th15: :: MATRIX12:15
for l, k, n, m being Nat
for K being Field
for M, M1 being Matrix of n,m,K st l in Seg (width M) &amp; k in Seg (width M) &amp; n > 0 &amp; m > 0 &amp; M1 = M @ holds
(ILine (M1,l,k)) @ = ICol (M,l,k)
proofend;

theorem Th16: :: MATRIX12:16
for l, n, m being Nat
for K being Field
for a being Element of K
for M, M1 being Matrix of n,m,K st l in Seg (width M) &amp; n > 0 &amp; m > 0 &amp; M1 = M @ holds
(SXLine (M1,l,a)) @ = SXCol (M,l,a)
proofend;

theorem Th17: :: MATRIX12:17
for l, k, n, m being Nat
for K being Field
for a being Element of K
for M, M1 being Matrix of n,m,K st l in Seg (width M) &amp; k in Seg (width M) &amp; n > 0 &amp; m > 0 &amp; M1 = M @ holds
(RLineXS (M1,l,k,a)) @ = RColXS (M,l,k,a)
proofend;

theorem :: MATRIX12:18
for l, n, k being Nat
for K being Field
for A being Matrix of n,K st l in dom (1. (K,n)) &amp; k in dom (1. (K,n)) &amp; n > 0 holds
A * (ICol ((1. (K,n)),l,k)) = ICol (A,l,k)
proofend;

theorem :: MATRIX12:19
for l, n being Nat
for K being Field
for a being Element of K
for A being Matrix of n,K st l in dom (1. (K,n)) &amp; n > 0 holds
A * (SXCol ((1. (K,n)),l,a)) = SXCol (A,l,a)
proofend;

theorem :: MATRIX12:20
for l, n, k being Nat
for K being Field
for a being Element of K
for A being Matrix of n,K st l in dom (1. (K,n)) &amp; k in dom (1. (K,n)) &amp; n > 0 holds
A * (RColXS ((1. (K,n)),l,k,a)) = RColXS (A,l,k,a)
proofend;

theorem :: MATRIX12:21
for l, n, k being Nat
for K being Field st l in dom (1. (K,n)) &amp; k in dom (1. (K,n)) &amp; n > 0 holds
(ICol ((1. (K,n)),l,k)) ~ = ICol ((1. (K,n)),l,k)
proofend;

theorem :: MATRIX12:22
for l, n, k being Nat
for K being Field
for a being Element of K st l in dom (1. (K,n)) &amp; k in dom (1. (K,n)) &amp; k <> l &amp; n > 0 holds
(RColXS ((1. (K,n)),l,k,a)) ~ = RColXS ((1. (K,n)),l,k,(- a))
proofend;

theorem :: MATRIX12:23
for l, n being Nat
for K being Field
for a being Element of K st l in dom (1. (K,n)) &amp; a <> 0. K &amp; n > 0 holds
(SXCol ((1. (K,n)),l,a)) ~ = SXCol ((1. (K,n)),l,(a "))
proofend;