let z0 be Element of REAL 2; :: thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_partial_differentiable_in z0,1 & f2 is_partial_differentiable_in z0,1 holds
f1 (#) f2 is_partial_differentiable_in z0,1
let f1, f2 be PartFunc of (REAL 2),REAL ; :: thesis: ( f1 is_partial_differentiable_in z0,1 & f2 is_partial_differentiable_in z0,1 implies f1 (#) f2 is_partial_differentiable_in z0,1 )
assume that
A1:
f1 is_partial_differentiable_in z0,1
and
A2:
f2 is_partial_differentiable_in z0,1
; :: thesis: f1 (#) f2 is_partial_differentiable_in z0,1
consider x0, y0 being Real such that
A3:
( z0 = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 1,f1,z0) & ex L being LINEAR ex R being REST st
for x being Real st x in N holds
((SVF1 1,f1,z0) . x) - ((SVF1 1,f1,z0) . x0) = (L . (x - x0)) + (R . (x - x0)) ) )
by A1, Def10;
consider N1 being Neighbourhood of x0 such that
A4:
( N1 c= dom (SVF1 1,f1,z0) & ex L being LINEAR ex R being REST st
for x being Real st x in N1 holds
((SVF1 1,f1,z0) . x) - ((SVF1 1,f1,z0) . x0) = (L . (x - x0)) + (R . (x - x0)) )
by A3;
consider L1 being LINEAR, R1 being REST such that
A5:
for x being Real st x in N1 holds
((SVF1 1,f1,z0) . x) - ((SVF1 1,f1,z0) . x0) = (L1 . (x - x0)) + (R1 . (x - x0))
by A4;
consider x1, y1 being Real such that
A6:
( z0 = <*x1,y1*> & ex N being Neighbourhood of x1 st
( N c= dom (SVF1 1,f2,z0) & ex L being LINEAR ex R being REST st
for x being Real st x in N holds
((SVF1 1,f2,z0) . x) - ((SVF1 1,f2,z0) . x1) = (L . (x - x1)) + (R . (x - x1)) ) )
by A2, Def10;
A7:
( x0 = x1 & y0 = y1 )
by A3, A6, FINSEQ_1:98;
consider N2 being Neighbourhood of x0 such that
A8:
( N2 c= dom (SVF1 1,f2,z0) & ex L being LINEAR ex R being REST st
for x being Real st x in N2 holds
((SVF1 1,f2,z0) . x) - ((SVF1 1,f2,z0) . x0) = (L . (x - x0)) + (R . (x - x0)) )
by A6, A7;
consider L2 being LINEAR, R2 being REST such that
A9:
for x being Real st x in N2 holds
((SVF1 1,f2,z0) . x) - ((SVF1 1,f2,z0) . x0) = (L2 . (x - x0)) + (R2 . (x - x0))
by A8;
consider N being Neighbourhood of x0 such that
A10:
( N c= N1 & N c= N2 )
by RCOMP_1:38;
reconsider L11 = ((SVF1 1,f2,z0) . x0) (#) L1, L12 = ((SVF1 1,f1,z0) . x0) (#) L2 as LINEAR by FDIFF_1:7;
A11:
( L11 is total & L12 is total & L1 is total & L2 is total )
by FDIFF_1:def 4;
reconsider L = L11 + L12 as LINEAR by FDIFF_1:6;
reconsider R11 = ((SVF1 1,f2,z0) . x0) (#) R1 as REST by FDIFF_1:9;
reconsider R12 = ((SVF1 1,f1,z0) . x0) (#) R2 as REST by FDIFF_1:9;
reconsider R13 = R11 + R12 as REST by FDIFF_1:8;
reconsider R14 = L1 (#) L2 as REST by FDIFF_1:10;
reconsider R15 = R13 + R14 as REST by FDIFF_1:8;
reconsider R16 = R1 (#) L2, R18 = R2 (#) L1 as REST by FDIFF_1:11;
reconsider R17 = R1 (#) R2 as REST by FDIFF_1:8;
reconsider R19 = R16 + R17 as REST by FDIFF_1:8;
reconsider R20 = R19 + R18 as REST by FDIFF_1:8;
reconsider R = R15 + R20 as REST by FDIFF_1:8;
A12:
( R1 is total & R2 is total & R11 is total & R12 is total & R13 is total & R14 is total & R15 is total & R16 is total & R17 is total & R18 is total & R19 is total & R20 is total )
by FDIFF_1:def 3;
A13:
N c= dom (SVF1 1,f1,z0)
by A4, A10, XBOOLE_1:1;
A14:
N c= dom (SVF1 1,f2,z0)
by A8, A10, XBOOLE_1:1;
AB:
for y being Real st y in N holds
y in dom (SVF1 1,(f1 (#) f2),z0)
proof
let y be
Real;
:: thesis: ( y in N implies y in dom (SVF1 1,(f1 (#) f2),z0) )
assume A15:
y in N
;
:: thesis: y in dom (SVF1 1,(f1 (#) f2),z0)
A16:
(
y in dom (reproj 1,z0) &
(reproj 1,z0) . y in dom f1 )
by A13, A15, FUNCT_1:21;
(
y in dom (reproj 1,z0) &
(reproj 1,z0) . y in dom f2 )
by A14, A15, FUNCT_1:21;
then
(
y in dom (reproj 1,z0) &
(reproj 1,z0) . y in (dom f1) /\ (dom f2) )
by A16, XBOOLE_0:def 4;
then
(
y in dom (reproj 1,z0) &
(reproj 1,z0) . y in dom (f1 (#) f2) )
by VALUED_1:def 4;
hence
y in dom (SVF1 1,(f1 (#) f2),z0)
by FUNCT_1:21;
:: thesis: verum
end;
then
for y being set st y in N holds
y in dom (SVF1 1,(f1 (#) f2),z0)
;
then A17:
N c= dom (SVF1 1,(f1 (#) f2),z0)
by TARSKI:def 3;
A18:
now let x be
Real;
:: thesis: ( x in N implies ((SVF1 1,(f1 (#) f2),z0) . x) - ((SVF1 1,(f1 (#) f2),z0) . x0) = (L . (x - x0)) + (R . (x - x0)) )assume A19:
x in N
;
:: thesis: ((SVF1 1,(f1 (#) f2),z0) . x) - ((SVF1 1,(f1 (#) f2),z0) . x0) = (L . (x - x0)) + (R . (x - x0))then A20:
(((SVF1 1,f1,z0) . x) - ((SVF1 1,f1,z0) . x0)) + ((SVF1 1,f1,z0) . x0) = ((L1 . (x - x0)) + (R1 . (x - x0))) + ((SVF1 1,f1,z0) . x0)
by A5, A10;
x in dom ((f1 (#) f2) * (reproj 1,z0))
by AB, A19;
then A21:
(
x in dom (reproj 1,z0) &
(reproj 1,z0) . x in dom (f1 (#) f2) )
by FUNCT_1:21;
then
(reproj 1,z0) . x in (dom f1) /\ (dom f2)
by VALUED_1:def 4;
then
(
(reproj 1,z0) . x in dom f1 &
(reproj 1,z0) . x in dom f2 )
by XBOOLE_0:def 4;
then A22:
(
x in dom (f1 * (reproj 1,z0)) &
x in dom (f2 * (reproj 1,z0)) )
by A21, FUNCT_1:21;
A23:
x0 in N
by RCOMP_1:37;
x0 in dom ((f1 (#) f2) * (reproj 1,z0))
by AB, RCOMP_1:37;
then A24:
(
x0 in dom (reproj 1,z0) &
(reproj 1,z0) . x0 in dom (f1 (#) f2) )
by FUNCT_1:21;
then
(reproj 1,z0) . x0 in (dom f1) /\ (dom f2)
by VALUED_1:def 4;
then
(
(reproj 1,z0) . x0 in dom f1 &
(reproj 1,z0) . x0 in dom f2 )
by XBOOLE_0:def 4;
then A25:
(
x0 in dom (f1 * (reproj 1,z0)) &
x0 in dom (f2 * (reproj 1,z0)) )
by A24, FUNCT_1:21;
thus ((SVF1 1,(f1 (#) f2),z0) . x) - ((SVF1 1,(f1 (#) f2),z0) . x0) =
((f1 (#) f2) . ((reproj 1,z0) . x)) - ((SVF1 1,(f1 (#) f2),z0) . x0)
by A17, A19, FUNCT_1:22
.=
((f1 . ((reproj 1,z0) . x)) * (f2 . ((reproj 1,z0) . x))) - ((SVF1 1,(f1 (#) f2),z0) . x0)
by VALUED_1:5
.=
(((SVF1 1,f1,z0) . x) * (f2 . ((reproj 1,z0) . x))) - ((SVF1 1,(f1 (#) f2),z0) . x0)
by A22, FUNCT_1:22
.=
(((SVF1 1,f1,z0) . x) * ((SVF1 1,f2,z0) . x)) - (((f1 (#) f2) * (reproj 1,z0)) . x0)
by A22, FUNCT_1:22
.=
(((SVF1 1,f1,z0) . x) * ((SVF1 1,f2,z0) . x)) - ((f1 (#) f2) . ((reproj 1,z0) . x0))
by A17, A23, FUNCT_1:22
.=
(((SVF1 1,f1,z0) . x) * ((SVF1 1,f2,z0) . x)) - ((f1 . ((reproj 1,z0) . x0)) * (f2 . ((reproj 1,z0) . x0)))
by VALUED_1:5
.=
(((SVF1 1,f1,z0) . x) * ((SVF1 1,f2,z0) . x)) - (((SVF1 1,f1,z0) . x0) * (f2 . ((reproj 1,z0) . x0)))
by A25, FUNCT_1:22
.=
(((((SVF1 1,f1,z0) . x) * ((SVF1 1,f2,z0) . x)) + (- (((SVF1 1,f1,z0) . x) * ((SVF1 1,f2,z0) . x0)))) + (((SVF1 1,f1,z0) . x) * ((SVF1 1,f2,z0) . x0))) - (((SVF1 1,f1,z0) . x0) * ((SVF1 1,f2,z0) . x0))
by A25, FUNCT_1:22
.=
(((SVF1 1,f1,z0) . x) * (((SVF1 1,f2,z0) . x) - ((SVF1 1,f2,z0) . x0))) + ((((SVF1 1,f1,z0) . x) - ((SVF1 1,f1,z0) . x0)) * ((SVF1 1,f2,z0) . x0))
.=
(((SVF1 1,f1,z0) . x) * (((SVF1 1,f2,z0) . x) - ((SVF1 1,f2,z0) . x0))) + (((L1 . (x - x0)) + (R1 . (x - x0))) * ((SVF1 1,f2,z0) . x0))
by A5, A10, A19
.=
(((SVF1 1,f1,z0) . x) * (((SVF1 1,f2,z0) . x) - ((SVF1 1,f2,z0) . x0))) + ((((SVF1 1,f2,z0) . x0) * (L1 . (x - x0))) + (((SVF1 1,f2,z0) . x0) * (R1 . (x - x0))))
.=
(((SVF1 1,f1,z0) . x) * (((SVF1 1,f2,z0) . x) - ((SVF1 1,f2,z0) . x0))) + ((L11 . (x - x0)) + (((SVF1 1,f2,z0) . x0) * (R1 . (x - x0))))
by A11, RFUNCT_1:73
.=
((((L1 . (x - x0)) + (R1 . (x - x0))) + ((SVF1 1,f1,z0) . x0)) * (((SVF1 1,f2,z0) . x) - ((SVF1 1,f2,z0) . x0))) + ((L11 . (x - x0)) + (R11 . (x - x0)))
by A12, A20, RFUNCT_1:73
.=
((((L1 . (x - x0)) + (R1 . (x - x0))) + ((SVF1 1,f1,z0) . x0)) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L11 . (x - x0)) + (R11 . (x - x0)))
by A9, A10, A19
.=
((((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((((SVF1 1,f1,z0) . x0) * (L2 . (x - x0))) + (((SVF1 1,f1,z0) . x0) * (R2 . (x - x0))))) + ((L11 . (x - x0)) + (R11 . (x - x0)))
.=
((((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L12 . (x - x0)) + (((SVF1 1,f1,z0) . x0) * (R2 . (x - x0))))) + ((L11 . (x - x0)) + (R11 . (x - x0)))
by A11, RFUNCT_1:73
.=
((((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L12 . (x - x0)) + (R12 . (x - x0)))) + ((L11 . (x - x0)) + (R11 . (x - x0)))
by A12, RFUNCT_1:73
.=
(((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L12 . (x - x0)) + ((L11 . (x - x0)) + ((R11 . (x - x0)) + (R12 . (x - x0)))))
.=
(((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L12 . (x - x0)) + ((L11 . (x - x0)) + (R13 . (x - x0))))
by A12, RFUNCT_1:72
.=
(((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + (((L11 . (x - x0)) + (L12 . (x - x0))) + (R13 . (x - x0)))
.=
((((L1 . (x - x0)) * (L2 . (x - x0))) + ((L1 . (x - x0)) * (R2 . (x - x0)))) + ((R1 . (x - x0)) * ((L2 . (x - x0)) + (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . (x - x0)))
by A11, RFUNCT_1:72
.=
(((R14 . (x - x0)) + ((R2 . (x - x0)) * (L1 . (x - x0)))) + ((R1 . (x - x0)) * ((L2 . (x - x0)) + (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . (x - x0)))
by A11, RFUNCT_1:72
.=
(((R14 . (x - x0)) + (R18 . (x - x0))) + (((R1 . (x - x0)) * (L2 . (x - x0))) + ((R1 . (x - x0)) * (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . (x - x0)))
by A11, A12, RFUNCT_1:72
.=
(((R14 . (x - x0)) + (R18 . (x - x0))) + ((R16 . (x - x0)) + ((R1 . (x - x0)) * (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . (x - x0)))
by A11, A12, RFUNCT_1:72
.=
(((R14 . (x - x0)) + (R18 . (x - x0))) + ((R16 . (x - x0)) + (R17 . (x - x0)))) + ((L . (x - x0)) + (R13 . (x - x0)))
by A12, RFUNCT_1:72
.=
(((R14 . (x - x0)) + (R18 . (x - x0))) + (R19 . (x - x0))) + ((L . (x - x0)) + (R13 . (x - x0)))
by A12, RFUNCT_1:72
.=
((R14 . (x - x0)) + ((R19 . (x - x0)) + (R18 . (x - x0)))) + ((L . (x - x0)) + (R13 . (x - x0)))
.=
((L . (x - x0)) + (R13 . (x - x0))) + ((R14 . (x - x0)) + (R20 . (x - x0)))
by A12, RFUNCT_1:72
.=
(L . (x - x0)) + (((R13 . (x - x0)) + (R14 . (x - x0))) + (R20 . (x - x0)))
.=
(L . (x - x0)) + ((R15 . (x - x0)) + (R20 . (x - x0)))
by A12, RFUNCT_1:72
.=
(L . (x - x0)) + (R . (x - x0))
by A12, RFUNCT_1:72
;
:: thesis: verum end;
thus
f1 (#) f2 is_partial_differentiable_in z0,1
by A3, A17, A18, Def10; :: thesis: verum