let L be non empty 1-sorted ; :: thesis: for N being non empty reflexive NetStr of L
for i, x being Element of N
for x1 being Element of (N | i) st x = x1 holds
N . x = (N | i) . x1
let N be non empty reflexive NetStr of L; :: thesis: for i, x being Element of N
for x1 being Element of (N | i) st x = x1 holds
N . x = (N | i) . x1
let i, x be Element of N; :: thesis: for x1 being Element of (N | i) st x = x1 holds
N . x = (N | i) . x1
let x1 be Element of (N | i); :: thesis: ( x = x1 implies N . x = (N | i) . x1 )
assume A1: x = x1 ; :: thesis: N . x = (N | i) . x1
thus N . x = (the mapping of N | the carrier of (N | i)) . x1 by A1, FUNCT_1:72
.= (N | i) . x1 by Def7 ; :: thesis: verum