theorem Th7: :: MFOLD_0:6

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