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