let L1, L2 be non empty 1-sorted ; ( the carrier of L1 = the carrier of L2 implies for N1 being NetStr over L1 ex N2 being strict NetStr over L2 st
( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) )
assume A1:
the carrier of L1 = the carrier of L2
; for N1 being NetStr over L1 ex N2 being strict NetStr over L2 st
( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 )
let N1 be NetStr over L1; ex N2 being strict NetStr over L2 st
( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 )
reconsider f = the mapping of N1 as Function of the carrier of N1, the carrier of L2 by A1;
take
NetStr(# the carrier of N1, the InternalRel of N1,f #)
; ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of NetStr(# the carrier of N1, the InternalRel of N1,f #), the InternalRel of NetStr(# the carrier of N1, the InternalRel of N1,f #) #) & the mapping of N1 = the mapping of NetStr(# the carrier of N1, the InternalRel of N1,f #) )
thus
( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of NetStr(# the carrier of N1, the InternalRel of N1,f #), the InternalRel of NetStr(# the carrier of N1, the InternalRel of N1,f #) #) & the mapping of N1 = the mapping of NetStr(# the carrier of N1, the InternalRel of N1,f #) )
; verum