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