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)) & n > 0 holds
(SXCol ((1. (K,n)),l,a)) ~ = SXCol ((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)) & n > 0 holds
(SXCol ((1. (K,n)),l,a)) ~ = SXCol ((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)) & n > 0 implies (SXCol ((1. (K,n)),l,a)) ~ = SXCol ((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)) and
A3: n > 0 ; :: thesis: (SXCol ((1. (K,n)),l,a)) ~ = SXCol ((1. (K,n)),l,(/ a))
A4: (SXLine ((1. (K,n)),l,a)) ~ = SXLine ((1. (K,n)),l,(/ a)) by A0, A1, Th14;
a3: SXLine ((1. (K,n)),l,a) is invertible by A0, A1, Th14;
( 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 SXCol ((1. (K,n)),l,(/ a)) = (SXLine ((1. (K,n)),l,(/ a))) @ by A1, A3, A5, Th16
.= ((SXLine ((1. (K,n)),l,a)) @) ~ by A4, MATRIX_6:13, a3
.= ((SXLine (((1. (K,n)) @),l,a)) @) ~ by MATRIX_6:10
.= (SXCol ((1. (K,n)),l,a)) ~ by A1, A3, A5, Th16 ;
hence (SXCol ((1. (K,n)),l,a)) ~ = SXCol ((1. (K,n)),l,(/ a)) ; :: thesis: verum