let R be non empty RelStr ; :: thesis: for T being non empty 1-sorted
for p being Element of T holds the_value_of (ConstantNet (R,p)) = p
let T be non empty 1-sorted ; :: thesis: for p being Element of T holds the_value_of (ConstantNet (R,p)) = p
let p be Element of T; :: thesis: the_value_of (ConstantNet (R,p)) = p
thus the_value_of (ConstantNet (R,p)) = the_value_of the mapping of (ConstantNet (R,p)) by Def8
.= the_value_of ( the carrier of (ConstantNet (R,p)) --> p) by Def5
.= p by FUNCOP_1:79 ; :: thesis: verum