let L1, L2 be non empty 1-sorted ; :: thesis: ( the carrier of L1 = the carrier of L2 implies for N1 being NetStr of L1 st N1 in NetUniv L1 holds
ex N2 being strict net of L2 st
( N2 in NetUniv L2 & 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 ; :: thesis: for N1 being NetStr of L1 st N1 in NetUniv L1 holds
ex N2 being strict net of L2 st
( N2 in NetUniv L2 & 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 of L1; :: thesis: ( N1 in NetUniv L1 implies ex N2 being strict net of L2 st
( N2 in NetUniv L2 & 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 N1 in NetUniv L1 ; :: thesis: ex N2 being strict net of L2 st
( N2 in NetUniv L2 & 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 )
then consider N being strict net of L1 such that
A2: ( N = N1 & the carrier of N in the_universe_of the carrier of L1 ) by YELLOW_6:def 14;
reconsider f = the mapping of N as Function of the carrier of N,the carrier of L2 by A1;
take NetStr(# the carrier of N,the InternalRel of N,f #) ; :: thesis: ( NetStr(# the carrier of N,the InternalRel of N,f #) in NetUniv L2 & RelStr(# the carrier of N1,the InternalRel of N1 #) = RelStr(# the carrier of NetStr(# the carrier of N,the InternalRel of N,f #),the InternalRel of NetStr(# the carrier of N,the InternalRel of N,f #) #) & the mapping of N1 = the mapping of NetStr(# the carrier of N,the InternalRel of N,f #) )
thus ( NetStr(# the carrier of N,the InternalRel of N,f #) in NetUniv L2 & RelStr(# the carrier of N1,the InternalRel of N1 #) = RelStr(# the carrier of NetStr(# the carrier of N,the InternalRel of N,f #),the InternalRel of NetStr(# the carrier of N,the InternalRel of N,f #) #) & the mapping of N1 = the mapping of NetStr(# the carrier of N,the InternalRel of N,f #) ) by A1, A2, YELLOW_6:def 14; :: thesis: verum