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 A1: ( l in dom (1. K,n) & 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;
set B = SXLine (1. K,n),l,(a " );
A2: (SXLine (1. K,n),l,a) * (SXLine (1. K,n),l,(a " )) = SXLine (SXLine (1. K,n),l,(a " )),l,a by A1, Th7;
A3: (SXLine (1. K,n),l,(a " )) * (SXLine (1. K,n),l,a) = SXLine (SXLine (1. K,n),l,a),l,(a " ) by A1, Th7, VECTSP_2:48;
A4: ( len (SXLine (1. K,n),l,a) = len (1. K,n) & width (SXLine (1. K,n),l,a) = width (1. K,n) ) by Def2, Th1;
A5: ( len (SXLine (1. K,n),l,(a " )) = len (1. K,n) & width (SXLine (1. K,n),l,(a " )) = width (1. K,n) ) by Def2, Th1;
A6: 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 ;
A7: 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 ;
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 [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 A8: ( i in dom (1. K,n) & j in Seg (width (1. K,n)) ) by ZFMISC_1:106;
then A9: ( (SXLine (SXLine (1. K,n),l,(a " )),l,a) * l,j = a * ((SXLine (1. K,n),l,(a " )) * l,j) & ( i <> l implies (SXLine (SXLine (1. K,n),l,(a " )),l,a) * i,j = (SXLine (1. K,n),l,(a " )) * i,j ) ) by A1, A5, A7, Def2;
A10: ( (SXLine (1. K,n),l,(a " )) * l,j = (a " ) * ((1. K,n) * l,j) & ( i <> l implies (SXLine (1. K,n),l,(a " )) * i,j = (1. K,n) * i,j ) ) by A1, A8, Def2;
then (SXLine (SXLine (1. K,n),l,(a " )),l,a) * l,j = a * ((a " ) * ((1. K,n) * l,j)) by A1, A5, A7, A8, Def2
.= (a * (a " )) * ((1. K,n) * l,j) by GROUP_1:def 4
.= (1_ K) * ((1. K,n) * l,j) by A1, VECTSP_2:def 7
.= (1. K,n) * l,j by GROUP_1:def 5 ;
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;
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 [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 A12: ( i in dom (1. K,n) & j in Seg (width (1. K,n)) ) by ZFMISC_1:106;
then A13: ( (SXLine (SXLine (1. K,n),l,a),l,(a " )) * l,j = (a " ) * ((SXLine (1. K,n),l,a) * l,j) & ( i <> l implies (SXLine (SXLine (1. K,n),l,a),l,(a " )) * i,j = (SXLine (1. K,n),l,a) * i,j ) ) by A1, A4, A6, Def2;
A14: ( (SXLine (1. K,n),l,a) * l,j = a * ((1. K,n) * l,j) & ( i <> l implies (SXLine (1. K,n),l,a) * i,j = (1. K,n) * i,j ) ) by A1, A12, Def2;
then (SXLine (SXLine (1. K,n),l,a),l,(a " )) * l,j = (a " ) * (a * ((1. K,n) * l,j)) by A1, A4, A6, A12, Def2
.= ((a " ) * a) * ((1. K,n) * l,j) by GROUP_1:def 4
.= (1_ K) * ((1. K,n) * l,j) by A1, VECTSP_2:def 7
.= (1. K,n) * l,j by GROUP_1:def 5 ;
hence (1. K,n) * i,j = (SXLine (SXLine (1. K,n),l,a),l,(a " )) * i,j by A13, A14; :: thesis: verum

end;

then 1. K,n = SXLine (SXLine (1. K,n),l,a),l,(a " ) by MATRIX_1:28;
then A15: SXLine (1. K,n),l,(a " ) is_reverse_of SXLine (1. K,n),l,a by A2, A3, A11, 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 A15, MATRIX_6:def 4; :: thesis: verum