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: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
.= (1_ K) * ((1. (K,n)) * (l,j)) by A2, VECTSP_2:def 2
.= (1. (K,n)) * (l,j) by GROUP_1:def 4 ;
( 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: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 A2, VECTSP_2:def 2
.= (1. (K,n)) * (l,j) by GROUP_1:def 4 ;
( 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: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