let l, n be Nat; :: thesis: for K being comRing
for a being Element of K st a is left_invertible & a is right_mult-cancelable & l in dom (1. (K,n)) holds
( SXLine ((1. (K,n)),l,a) is invertible & (SXLine ((1. (K,n)),l,a)) ~ = SXLine ((1. (K,n)),l,(/ a)) )
let K be comRing; :: thesis: for a being Element of K st a is left_invertible & a is right_mult-cancelable & l in dom (1. (K,n)) 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: ( a is left_invertible & a is right_mult-cancelable & l in dom (1. (K,n)) implies ( SXLine ((1. (K,n)),l,a) is invertible & (SXLine ((1. (K,n)),l,a)) ~ = SXLine ((1. (K,n)),l,(/ a)) ) )
assume that
A0: ( a is left_invertible & a is right_mult-cancelable ) and
A1: l in dom (1. (K,n)) ; :: 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:87;
A8: j in Seg (width (1. (K,n))) by A6, ZFMISC_1:87;
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 3
.= ((/ a) * a) * ((1. (K,n)) * (l,j))
.= (1_ K) * ((1. (K,n)) * (l,j)) by A0, ALGSTR_0:def 30
.= (1. (K,n)) * (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 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_0:27;
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:87;
A15: j in Seg (width (1. (K,n))) by A13, ZFMISC_1:87;
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 3
.= (1_ K) * ((1. (K,n)) * (l,j)) by A0, ALGSTR_0:def 30
.= (1. (K,n)) * (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 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_0:27;
( (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