theorem Th9: :: MFOLD_0:9

for N, M being non empty locally_euclidean TopSpace holds Fr [:N,M:] = [:([#] N),(Fr M):] \/ [:(Fr N),([#] M):]