let k, l, n be Nat; :: thesis: for K being comRing
for a being Element of K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & k <> l & n > 0 holds
(RColXS ((1. (K,n)),l,k,a)) ~ = RColXS ((1. (K,n)),l,k,(- a))
let K be comRing; :: thesis: for a being Element of K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & k <> l & n > 0 holds
(RColXS ((1. (K,n)),l,k,a)) ~ = RColXS ((1. (K,n)),l,k,(- a))
let a be Element of K; :: thesis: ( l in dom (1. (K,n)) & k in dom (1. (K,n)) & k <> l & n > 0 implies (RColXS ((1. (K,n)),l,k,a)) ~ = RColXS ((1. (K,n)),l,k,(- a)) )
assume that
A1: ( l in dom (1. (K,n)) & k in dom (1. (K,n)) ) and
A2: k <> l and
A3: n > 0 ; :: thesis: (RColXS ((1. (K,n)),l,k,a)) ~ = RColXS ((1. (K,n)),l,k,(- a))
A4: (RLineXS ((1. (K,n)),l,k,a)) ~ = RLineXS ((1. (K,n)),l,k,(- a)) by A1, A2, Th13;
a3: RLineXS ((1. (K,n)),l,k,a) is invertible by A1, Th13, A2;
( len (1. (K,n)) = n & width (1. (K,n)) = n ) by MATRIX_0:24;
then A5: dom (1. (K,n)) = Seg (width (1. (K,n))) by FINSEQ_1:def 3;
(1. (K,n)) @ = 1. (K,n) by MATRIX_6:10;
then RColXS ((1. (K,n)),l,k,(- a)) = (RLineXS ((1. (K,n)),l,k,(- a))) @ by A1, A3, A5, Th17
.= ((RLineXS ((1. (K,n)),l,k,a)) @) ~ by A4, MATRIX_6:13, a3
.= ((RLineXS (((1. (K,n)) @),l,k,a)) @) ~ by MATRIX_6:10
.= (RColXS ((1. (K,n)),l,k,a)) ~ by A1, A3, A5, Th17 ;
hence (RColXS ((1. (K,n)),l,k,a)) ~ = RColXS ((1. (K,n)),l,k,(- a)) ; :: thesis: verum