take NetStr(# the carrier of N,the InternalRel of N,(f * the mapping of N) #) ; :: thesis: ( RelStr(# the carrier of NetStr(# the carrier of N,the InternalRel of N,(f * the mapping of N) #),the InternalRel of NetStr(# the carrier of N,the InternalRel of N,(f * the mapping of N) #) #) = RelStr(# the carrier of N,the InternalRel of N #) & the mapping of NetStr(# the carrier of N,the InternalRel of N,(f * the mapping of N) #) = f * the mapping of N )
thus ( RelStr(# the carrier of NetStr(# the carrier of N,the InternalRel of N,(f * the mapping of N) #),the InternalRel of NetStr(# the carrier of N,the InternalRel of N,(f * the mapping of N) #) #) = RelStr(# the carrier of N,the InternalRel of N #) & the mapping of NetStr(# the carrier of N,the InternalRel of N,(f * the mapping of N) #) = f * the mapping of N ) ; :: thesis: verum