let i, j, n be Nat; :: thesis: for K being non empty doubleLoopStr st [i,j] in Indices (0. (K,n)) holds

(0. (K,n)) * (i,j) = 0. K

let K be non empty doubleLoopStr ; :: thesis: ( [i,j] in Indices (0. (K,n)) implies (0. (K,n)) * (i,j) = 0. K )

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

set M = 0. (K,n);

assume A1: [i,j] in Indices (0. (K,n)) ; :: thesis: (0. (K,n)) * (i,j) = 0. K

then A2: [i,j] in [:(Seg n),(Seg n):] by MATRIX_0:24;

then j in Seg n by ZFMISC_1:87;

then A3: (n1 |-> (0. K)) . j = 0. K by FUNCOP_1:7;

i in Seg n by A2, ZFMISC_1:87;

then (0. (K,n)) . i = n1 |-> (0. K) by FUNCOP_1:7;

hence (0. (K,n)) * (i,j) = 0. K by A1, A3, MATRIX_0:def 5; :: thesis: verum

(0. (K,n)) * (i,j) = 0. K

let K be non empty doubleLoopStr ; :: thesis: ( [i,j] in Indices (0. (K,n)) implies (0. (K,n)) * (i,j) = 0. K )

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

set M = 0. (K,n);

assume A1: [i,j] in Indices (0. (K,n)) ; :: thesis: (0. (K,n)) * (i,j) = 0. K

then A2: [i,j] in [:(Seg n),(Seg n):] by MATRIX_0:24;

then j in Seg n by ZFMISC_1:87;

then A3: (n1 |-> (0. K)) . j = 0. K by FUNCOP_1:7;

i in Seg n by A2, ZFMISC_1:87;

then (0. (K,n)) . i = n1 |-> (0. K) by FUNCOP_1:7;

hence (0. (K,n)) * (i,j) = 0. K by A1, A3, MATRIX_0:def 5; :: thesis: verum