let X, T be Subset of REAL; :: thesis: 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) ) )
let f, g be PartFunc of REAL,REAL; :: thesis: ( X c= dom f & T c= dom g implies 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) ) ) )
assume ( X c= dom f & T c= dom g ) ; :: thesis: 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) ) )
defpred S₁[ object , object ] means ex x, t being Real st
( x in X & t in T & $1 = <*x,t*> & $2 = (f /. x) * (g /. t) );
P1: for z, w being object st z in REAL 2 & S₁[z,w] holds
w in REAL ;
P2: for z, w1, w2 being object st z in REAL 2 & S₁[z,w1] & S₁[z,w2] holds
w1 = w2

proof

let z, w1, w2 be object ; :: thesis: ( z in REAL 2 & S₁[z,w1] & S₁[z,w2] implies w1 = w2 )
assume that
z in REAL 2 and
P21: S₁[z,w1] and
P22: S₁[z,w2] ; :: thesis: w1 = w2
consider x1, t1 being Real such that
P23: ( z = <*x1,t1*> & w1 = (f /. x1) * (g /. t1) ) by P21;
consider x2, t2 being Real such that
P24: ( z = <*x2,t2*> & w2 = (f /. x2) * (g /. t2) ) by P22;
( x1 = x2 & t1 = t2 ) by P23, P24, FINSEQ_1:77;
hence w1 = w2 by P23, P24; :: thesis: verum

end;

consider u being PartFunc of (REAL 2),REAL such that
P3: for z being object holds
( z in dom u iff ( z in REAL 2 & ex w being object st S₁[z,w] ) ) and
P4: for z being object st z in dom u holds
S₁[z,u . z] from PARTFUN1:sch 2(P1, P2);
take u ; :: thesis: ( 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) ) )
for z being object holds
( z in dom u iff z in { <*x,t*> where x, t is Real : ( x in X & t in T ) } )

proof

let z be object ; :: thesis: ( z in dom u iff z in { <*x,t*> where x, t is Real : ( x in X & t in T ) } )

hereby :: thesis: ( z in { <*x,t*> where x, t is Real : ( x in X & t in T ) } implies z in dom u )

assume z in dom u ; :: thesis: z in { <*x,t*> where x, t is Real : ( x in X & t in T ) }
then ( z in REAL 2 & ex w being object st S₁[z,w] ) by P3;
hence z in { <*x,t*> where x, t is Real : ( x in X & t in T ) } ; :: thesis: verum

end;

assume z in { <*x,t*> where x, t is Real : ( x in X & t in T ) } ; :: thesis: z in dom u
then consider x, t being Real such that
P51: ( z = <*x,t*> & x in X & t in T ) ;
(f /. x) * (g /. t) in REAL ;
hence z in dom u by P3, P51, LM02; :: thesis: verum

end;

hence P5: dom u = { <*x,t*> where x, t is Real : ( x in X & t in T ) } by TARSKI:2; :: thesis: for x, t being Real st x in X & t in T holds
u /. <*x,t*> = (f /. x) * (g /. t)
let x, t be Real; :: thesis: ( x in X & t in T implies u /. <*x,t*> = (f /. x) * (g /. t) )
assume ( x in X & t in T ) ; :: thesis: u /. <*x,t*> = (f /. x) * (g /. t)
then P7: <*x,t*> in dom u by P5;
then consider x1, t1 being Real such that
( x1 in X & t1 in T ) and
P9: <*x,t*> = <*x1,t1*> and
P10: u . <*x,t*> = (f /. x1) * (g /. t1) by P4;
( x = x1 & t = t1 ) by P9, FINSEQ_1:77;
hence u /. <*x,t*> = (f /. x) * (g /. t) by P10, P7, PARTFUN1:def 6; :: thesis: verum