let R be non empty RelStr ; for T being non empty 1-sorted
for p being Element of T
for q being Element of (ConstantNet (R,p)) holds (ConstantNet (R,p)) . q = p
let T be non empty 1-sorted ; for p being Element of T
for q being Element of (ConstantNet (R,p)) holds (ConstantNet (R,p)) . q = p
let p be Element of T; for q being Element of (ConstantNet (R,p)) holds (ConstantNet (R,p)) . q = p
let q be Element of (ConstantNet (R,p)); (ConstantNet (R,p)) . q = p
thus (ConstantNet (R,p)) . q =
( the carrier of (ConstantNet (R,p)) --> p) . q
by Def5
.=
p
; verum