let l, n, k be Nat; :: thesis: for K being Field st l in dom (1. K,n) & k in dom (1. K,n) & n > 0 holds
(ICol (1. K,n),l,k) ~ = ICol (1. K,n),l,k
let K be Field; :: thesis: ( l in dom (1. K,n) & k in dom (1. K,n) & n > 0 implies (ICol (1. K,n),l,k) ~ = ICol (1. K,n),l,k )
assume that
A1: ( l in dom (1. K,n) & k in dom (1. K,n) ) and
A2: n > 0 ; :: thesis: (ICol (1. K,n),l,k) ~ = ICol (1. K,n),l,k
A3: (ILine (1. K,n),l,k) ~ = ILine (1. K,n),l,k by A1, Th12;
( len (1. K,n) = n & width (1. K,n) = n ) by MATRIX_1:25;
then A4: 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 ICol (1. K,n),l,k = (ILine (1. K,n),l,k) @ by A1, A2, A4, Th15
.= ((ILine (1. K,n),l,k) @ ) ~ by A1, A2, A3, Th12, MATRIX_6:13
.= ((ILine ((1. K,n) @ ),l,k) @ ) ~ by MATRIX_6:10
.= (ICol (1. K,n),l,k) ~ by A1, A2, A4, Th15 ;
hence (ICol (1. K,n),l,k) ~ = ICol (1. K,n),l,k ; :: thesis: verum