let L be non empty 1-sorted ; :: thesis: for N being non empty directed NetStr over 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 directed NetStr over 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 x = x1 ; :: thesis: N . x = (N | i) . x1
hence N . x = ( the mapping of N | the carrier of (N | i)) . x1 by FUNCT_1:49
.= (N | i) . x1 by Def7 ;
:: thesis: verum