let l, n, k be Nat; :: thesis: for K being Field
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 Field; :: 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;
( len (1. K,n) = n & width (1. K,n) = n ) by MATRIX_1:25;
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 A1, A2, A3, A4, Th13, MATRIX_6:13
.= ((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