let R be non empty RelStr ; :: thesis: 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 ; :: thesis: 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; :: thesis: for q being Element of (ConstantNet R,p) holds (ConstantNet R,p) . q = p
let q be Element of (ConstantNet R,p); :: thesis: (ConstantNet R,p) . q = p
thus (ConstantNet R,p) . q = (the carrier of (ConstantNet R,p) --> p) . q by Def7
.= p by FUNCOP_1:13 ; :: thesis: verum