let f, g be PartFunc of REAL,REAL; for u being PartFunc of (REAL 2),REAL
for x0, t0 being Real
for z being Element of REAL 2 st dom u = { <*x,t*> where x, t is Real : ( x in dom f & t in dom g ) } & ( for x, t being Real st x in dom f & t in dom g holds
u /. <*x,t*> = (f /. x) * (g /. t) ) & z = <*x0,t0*> & x0 in dom f & t0 in dom g holds
( u * (reproj (1,z)) = (g /. t0) (#) f & u * (reproj (2,z)) = (f /. x0) (#) g )
let u be PartFunc of (REAL 2),REAL; for x0, t0 being Real
for z being Element of REAL 2 st dom u = { <*x,t*> where x, t is Real : ( x in dom f & t in dom g ) } & ( for x, t being Real st x in dom f & t in dom g holds
u /. <*x,t*> = (f /. x) * (g /. t) ) & z = <*x0,t0*> & x0 in dom f & t0 in dom g holds
( u * (reproj (1,z)) = (g /. t0) (#) f & u * (reproj (2,z)) = (f /. x0) (#) g )
let x0, t0 be Real; for z being Element of REAL 2 st dom u = { <*x,t*> where x, t is Real : ( x in dom f & t in dom g ) } & ( for x, t being Real st x in dom f & t in dom g holds
u /. <*x,t*> = (f /. x) * (g /. t) ) & z = <*x0,t0*> & x0 in dom f & t0 in dom g holds
( u * (reproj (1,z)) = (g /. t0) (#) f & u * (reproj (2,z)) = (f /. x0) (#) g )
let z be Element of REAL 2; ( dom u = { <*x,t*> where x, t is Real : ( x in dom f & t in dom g ) } & ( for x, t being Real st x in dom f & t in dom g holds
u /. <*x,t*> = (f /. x) * (g /. t) ) & z = <*x0,t0*> & x0 in dom f & t0 in dom g implies ( u * (reproj (1,z)) = (g /. t0) (#) f & u * (reproj (2,z)) = (f /. x0) (#) g ) )
assume that
AS1:
dom u = { <*x,t*> where x, t is Real : ( x in dom f & t in dom g ) }
and
AS2:
for x, t being Real st x in dom f & t in dom g holds
u /. <*x,t*> = (f /. x) * (g /. t)
and
AS3:
( z = <*x0,t0*> & x0 in dom f & t0 in dom g )
; ( u * (reproj (1,z)) = (g /. t0) (#) f & u * (reproj (2,z)) = (f /. x0) (#) g )
P21:
for s being object holds
( s in dom (u * (reproj (1,z))) iff s in dom f )
proof
let s be
object ;
( s in dom (u * (reproj (1,z))) iff s in dom f )
hereby ( s in dom f implies s in dom (u * (reproj (1,z))) )
assume P10:
s in dom (u * (reproj (1,z)))
;
s in dom fthen reconsider r =
s as
Real ;
A4a:
r is
Element of
REAL
by XREAL_0:def 1;
(reproj (1,z)) . r =
Replace (
z,1,
r)
by PDIFF_1:def 5, A4a
.=
<*r,t0*>
by AS3, FINSEQ_7:13, A4a
;
then
<*r,t0*> in { <*x,t*> where x, t is Real : ( x in dom f & t in dom g ) }
by P10, FUNCT_1:11, AS1;
then
ex
x,
t being
Real st
(
<*r,t0*> = <*x,t*> &
x in dom f &
t in dom g )
;
hence
s in dom f
by FINSEQ_1:77;
verum
end;
assume P12:
s in dom f
;
s in dom (u * (reproj (1,z)))
then reconsider r =
s as
Real ;
P13:
s in REAL
by P12;
P14:
(reproj (1,z)) . r =
Replace (
z,1,
r)
by PDIFF_1:def 5, P12
.=
<*r,t0*>
by AS3, FINSEQ_7:13, P12
;
P15:
(reproj (1,z)) . s in dom u
by P12, P14, AS1, AS3;
s in dom (reproj (1,z))
by P13, FUNCT_2:def 1;
hence
s in dom (u * (reproj (1,z)))
by P15, FUNCT_1:11;
verum
end;
then P2:
dom (u * (reproj (1,z))) = dom f
by TARSKI:2;
P31:
for s being object holds
( s in dom (u * (reproj (2,z))) iff s in dom g )
proof
let s be
object ;
( s in dom (u * (reproj (2,z))) iff s in dom g )
hereby ( s in dom g implies s in dom (u * (reproj (2,z))) )
assume P10:
s in dom (u * (reproj (2,z)))
;
s in dom gthen reconsider r =
s as
Real ;
A4:
r is
Element of
REAL
by XREAL_0:def 1;
(reproj (2,z)) . r =
Replace (
z,2,
r)
by PDIFF_1:def 5, A4
.=
<*x0,r*>
by AS3, FINSEQ_7:14, A4
;
then
<*x0,r*> in { <*x,t*> where x, t is Real : ( x in dom f & t in dom g ) }
by P10, FUNCT_1:11, AS1;
then
ex
x,
t being
Real st
(
<*x0,r*> = <*x,t*> &
x in dom f &
t in dom g )
;
hence
s in dom g
by FINSEQ_1:77;
verum
end;
assume P12:
s in dom g
;
s in dom (u * (reproj (2,z)))
then reconsider r =
s as
Real ;
P14:
(reproj (2,z)) . r =
Replace (
z,2,
r)
by PDIFF_1:def 5, P12
.=
<*x0,r*>
by AS3, FINSEQ_7:14, P12
;
P15:
<*x0,r*> in { <*x,t*> where x, t is Real : ( x in dom f & t in dom g ) }
by P12, AS3;
s in REAL
by P12;
then
s in dom (reproj (2,z))
by FUNCT_2:def 1;
hence
s in dom (u * (reproj (2,z)))
by P15, P14, AS1, FUNCT_1:11;
verum
end;
P4:
dom ((g /. t0) (#) f) = dom f
by VALUED_1:def 5;
P5:
dom ((f /. x0) (#) g) = dom g
by VALUED_1:def 5;
for s being object st s in dom (u * (reproj (1,z))) holds
(u * (reproj (1,z))) . s = ((g /. t0) (#) f) . s
proof
let s be
object ;
( s in dom (u * (reproj (1,z))) implies (u * (reproj (1,z))) . s = ((g /. t0) (#) f) . s )
assume A1:
s in dom (u * (reproj (1,z)))
;
(u * (reproj (1,z))) . s = ((g /. t0) (#) f) . s
then reconsider r =
s as
Real ;
A3:
<*r,t0*> in dom u
by P2, A1, AS3, AS1;
A4a:
r is
Element of
REAL
by XREAL_0:def 1;
thus (u * (reproj (1,z))) . s =
u . ((reproj (1,z)) . r)
by FUNCT_1:12, A1
.=
u . (Replace (z,1,r))
by PDIFF_1:def 5, A4a
.=
u . <*r,t0*>
by AS3, FINSEQ_7:13, A4a
.=
u /. <*r,t0*>
by A3, PARTFUN1:def 6
.=
(f /. r) * (g /. t0)
by A1, AS3, AS2, P21
.=
(f . r) * (g /. t0)
by PARTFUN1:def 6, A1, P21
.=
((g /. t0) (#) f) . s
by VALUED_1:def 5, A1, P21, P4
;
verum
end;
hence
u * (reproj (1,z)) = (g /. t0) (#) f
by FUNCT_1:2, P21, TARSKI:2, P4; u * (reproj (2,z)) = (f /. x0) (#) g
for s being object st s in dom (u * (reproj (2,z))) holds
(u * (reproj (2,z))) . s = ((f /. x0) (#) g) . s
proof
let s be
object ;
( s in dom (u * (reproj (2,z))) implies (u * (reproj (2,z))) . s = ((f /. x0) (#) g) . s )
assume A1:
s in dom (u * (reproj (2,z)))
;
(u * (reproj (2,z))) . s = ((f /. x0) (#) g) . s
then reconsider r =
s as
Real ;
s in dom g
by P31, A1;
then A3:
<*x0,r*> in dom u
by AS3, AS1;
A4a:
r is
Element of
REAL
by XREAL_0:def 1;
thus (u * (reproj (2,z))) . s =
u . ((reproj (2,z)) . r)
by FUNCT_1:12, A1
.=
u . (Replace (z,2,r))
by PDIFF_1:def 5, A4a
.=
u . <*x0,r*>
by AS3, FINSEQ_7:14, A4a
.=
u /. <*x0,r*>
by A3, PARTFUN1:def 6
.=
(f /. x0) * (g /. r)
by P31, A1, AS3, AS2
.=
(g . r) * (f /. x0)
by PARTFUN1:def 6, P31, A1
.=
((f /. x0) (#) g) . s
by VALUED_1:def 5, P31, A1, P5
;
verum
end;
hence
u * (reproj (2,z)) = (f /. x0) (#) g
by FUNCT_1:2, P31, TARSKI:2, P5; verum