let S be non empty 1-sorted ; :: thesis: for e being Element of
for x being Element of holds (Net-Str e) . x = e
let e be Element of ; :: thesis: for x being Element of holds (Net-Str e) . x = e
let x be Element of ; :: 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, FUNCT_1:35 ; :: thesis: verum