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 13;
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 Th25;
then j in Seg n by ZFMISC_1:106;
then A3: (n1 |-> (0. K)) . j = 0. K by FUNCOP_1:13;
i in Seg n by A2, ZFMISC_1:106;
then (0. K,n) . i = n1 |-> (0. K) by FUNCOP_1:13;
hence (0. K,n) * i,j = 0. K by A1, A3, Def6; :: thesis: verum