let S be non empty 1-sorted ; :: thesis: for e being Element of S
for x being Element of (Net-Str e) holds (Net-Str e) . x = e
let e be Element of S; :: thesis: for x being Element of (Net-Str e) holds (Net-Str e) . x = e
let x be Element of (Net-Str e); :: thesis: (Net-Str e) . x = e
set N = Net-Str e;
A1: the carrier of (Net-Str e) = {e} by Def11;
then A2: x = e by TARSKI:def 1;
thus (Net-Str e) . x = (id {e}) . x by Def11
.= e by A1, A2 ; :: thesis: verum