let l, n be Nat; :: thesis: for K being Field
for a being Element of K st l in dom (1. K,n) & a <> 0. K holds
( SXLine (1. K,n),l,a is invertible & (SXLine (1. K,n),l,a) ~ = SXLine (1. K,n),l,(a " ) )
let K be Field; :: thesis: for a being Element of K st l in dom (1. K,n) & a <> 0. K holds
( SXLine (1. K,n),l,a is invertible & (SXLine (1. K,n),l,a) ~ = SXLine (1. K,n),l,(a " ) )
let a be Element of K; :: thesis: ( l in dom (1. K,n) & a <> 0. K implies ( SXLine (1. K,n),l,a is invertible & (SXLine (1. K,n),l,a) ~ = SXLine (1. K,n),l,(a " ) ) )
assume that
A1: l in dom (1. K,n) and
A2: a <> 0. K ; :: thesis: ( SXLine (1. K,n),l,a is invertible & (SXLine (1. K,n),l,a) ~ = SXLine (1. K,n),l,(a " ) )
set A = SXLine (1. K,n),l,a;
A3: dom (SXLine (1. K,n),l,a) = Seg (len (SXLine (1. K,n),l,a)) by FINSEQ_1:def 3
.= Seg (len (1. K,n)) by Def2
.= dom (1. K,n) by FINSEQ_1:def 3 ;
set B = SXLine (1. K,n),l,(a " );
A4: dom (SXLine (1. K,n),l,(a " )) = Seg (len (SXLine (1. K,n),l,(a " ))) by FINSEQ_1:def 3
.= Seg (len (1. K,n)) by Def2
.= dom (1. K,n) by FINSEQ_1:def 3 ;
A5: width (SXLine (1. K,n),l,(a " )) = width (1. K,n) by Th1;
for i, j being Nat st [i,j] in Indices (1. K,n) holds
(1. K,n) * i,j = (SXLine (SXLine (1. K,n),l,(a " )),l,a) * i,j

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (1. K,n) implies (1. K,n) * i,j = (SXLine (SXLine (1. K,n),l,(a " )),l,a) * i,j )
assume A6: [i,j] in Indices (1. K,n) ; :: thesis: (1. K,n) * i,j = (SXLine (SXLine (1. K,n),l,(a " )),l,a) * i,j
then A7: i in dom (1. K,n) by ZFMISC_1:106;
A8: j in Seg (width (1. K,n)) by A6, ZFMISC_1:106;
then A9: ( i <> l implies (SXLine (1. K,n),l,(a " )) * i,j = (1. K,n) * i,j ) by A7, Def2;
(SXLine (1. K,n),l,(a " )) * l,j = (a " ) * ((1. K,n) * l,j) by A1, A8, Def2;
then A10: (SXLine (SXLine (1. K,n),l,(a " )),l,a) * l,j = a * ((a " ) * ((1. K,n) * l,j)) by A1, A5, A4, A8, Def2
.= (a * (a " )) * ((1. K,n) * l,j) by GROUP_1:def 4
.= (1_ K) * ((1. K,n) * l,j) by A2, VECTSP_2:def 7
.= (1. K,n) * l,j by GROUP_1:def 5 ;
( i <> l implies (SXLine (SXLine (1. K,n),l,(a " )),l,a) * i,j = (SXLine (1. K,n),l,(a " )) * i,j ) by A5, A4, A7, A8, Def2;
hence (1. K,n) * i,j = (SXLine (SXLine (1. K,n),l,(a " )),l,a) * i,j by A9, A10; :: thesis: verum

end;

then A11: 1. K,n = SXLine (SXLine (1. K,n),l,(a " )),l,a by MATRIX_1:28;
A12: width (SXLine (1. K,n),l,a) = width (1. K,n) by Th1;
for i, j being Nat st [i,j] in Indices (1. K,n) holds
(1. K,n) * i,j = (SXLine (SXLine (1. K,n),l,a),l,(a " )) * i,j

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (1. K,n) implies (1. K,n) * i,j = (SXLine (SXLine (1. K,n),l,a),l,(a " )) * i,j )
assume A13: [i,j] in Indices (1. K,n) ; :: thesis: (1. K,n) * i,j = (SXLine (SXLine (1. K,n),l,a),l,(a " )) * i,j
then A14: i in dom (1. K,n) by ZFMISC_1:106;
A15: j in Seg (width (1. K,n)) by A13, ZFMISC_1:106;
then A16: ( i <> l implies (SXLine (1. K,n),l,a) * i,j = (1. K,n) * i,j ) by A14, Def2;
(SXLine (1. K,n),l,a) * l,j = a * ((1. K,n) * l,j) by A1, A15, Def2;
then A17: (SXLine (SXLine (1. K,n),l,a),l,(a " )) * l,j = (a " ) * (a * ((1. K,n) * l,j)) by A1, A12, A3, A15, Def2
.= ((a " ) * a) * ((1. K,n) * l,j) by GROUP_1:def 4
.= (1_ K) * ((1. K,n) * l,j) by A2, VECTSP_2:def 7
.= (1. K,n) * l,j by GROUP_1:def 5 ;
( i <> l implies (SXLine (SXLine (1. K,n),l,a),l,(a " )) * i,j = (SXLine (1. K,n),l,a) * i,j ) by A12, A3, A14, A15, Def2;
hence (1. K,n) * i,j = (SXLine (SXLine (1. K,n),l,a),l,(a " )) * i,j by A16, A17; :: thesis: verum

end;

then A18: 1. K,n = SXLine (SXLine (1. K,n),l,a),l,(a " ) by MATRIX_1:28;
( (SXLine (1. K,n),l,a) * (SXLine (1. K,n),l,(a " )) = SXLine (SXLine (1. K,n),l,(a " )),l,a & (SXLine (1. K,n),l,(a " )) * (SXLine (1. K,n),l,a) = SXLine (SXLine (1. K,n),l,a),l,(a " ) ) by A1, Th7;
then A19: SXLine (1. K,n),l,(a " ) is_reverse_of SXLine (1. K,n),l,a by A11, A18, MATRIX_6:def 2;
then SXLine (1. K,n),l,a is invertible by MATRIX_6:def 3;
hence ( SXLine (1. K,n),l,a is invertible & (SXLine (1. K,n),l,a) ~ = SXLine (1. K,n),l,(a " ) ) by A19, MATRIX_6:def 4; :: thesis: verum