theorem LM10: :: PDIFFEQ1:7

for X, T being Subset of REAL
for f, g being PartFunc of REAL,REAL st X c= dom f & T c= dom g holds
ex u being PartFunc of (REAL 2),REAL st
( dom u = { <*x,t*> where x, t is Real : ( x in X & t in T ) } & ( for x, t being Real st x in X & t in T holds
u /. <*x,t*> = (f /. x) * (g /. t) ) )