let u0 be Element of REAL 3; for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_partial_differentiable_in u0,3 & f2 is_partial_differentiable_in u0,3 holds
f1 (#) f2 is_partial_differentiable_in u0,3
let f1, f2 be PartFunc of (REAL 3),REAL; ( f1 is_partial_differentiable_in u0,3 & f2 is_partial_differentiable_in u0,3 implies f1 (#) f2 is_partial_differentiable_in u0,3 )
assume that
A1:
f1 is_partial_differentiable_in u0,3
and
A2:
f2 is_partial_differentiable_in u0,3
; f1 (#) f2 is_partial_differentiable_in u0,3
consider x0, y0, z0 being Real such that
A3:
( u0 = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f1,u0)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N holds
((SVF1 (3,f1,u0)) . z) - ((SVF1 (3,f1,u0)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) )
by A1, Th15;
consider N1 being Neighbourhood of z0 such that
A4:
( N1 c= dom (SVF1 (3,f1,u0)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N1 holds
((SVF1 (3,f1,u0)) . z) - ((SVF1 (3,f1,u0)) . z0) = (L . (z - z0)) + (R . (z - z0)) )
by A3;
consider L1 being LinearFunc, R1 being RestFunc such that
A5:
for z being Real st z in N1 holds
((SVF1 (3,f1,u0)) . z) - ((SVF1 (3,f1,u0)) . z0) = (L1 . (z - z0)) + (R1 . (z - z0))
by A4;
consider x1, y1, z1 being Real such that
A6:
( u0 = <*x1,y1,z1*> & ex N being Neighbourhood of z1 st
( N c= dom (SVF1 (3,f2,u0)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N holds
((SVF1 (3,f2,u0)) . z) - ((SVF1 (3,f2,u0)) . z1) = (L . (z - z1)) + (R . (z - z1)) ) )
by A2, Th15;
( x0 = x1 & y0 = y1 & z0 = z1 )
by A3, A6, FINSEQ_1:78;
then consider N2 being Neighbourhood of z0 such that
A7:
( N2 c= dom (SVF1 (3,f2,u0)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N2 holds
((SVF1 (3,f2,u0)) . z) - ((SVF1 (3,f2,u0)) . z0) = (L . (z - z0)) + (R . (z - z0)) )
by A6;
consider L2 being LinearFunc, R2 being RestFunc such that
A8:
for z being Real st z in N2 holds
((SVF1 (3,f2,u0)) . z) - ((SVF1 (3,f2,u0)) . z0) = (L2 . (z - z0)) + (R2 . (z - z0))
by A7;
consider N being Neighbourhood of z0 such that
A9:
( N c= N1 & N c= N2 )
by RCOMP_1:17;
reconsider L11 = ((SVF1 (3,f2,u0)) . z0) (#) L1 as LinearFunc by FDIFF_1:3;
reconsider L12 = ((SVF1 (3,f1,u0)) . z0) (#) L2 as LinearFunc by FDIFF_1:3;
A10:
( L11 is total & L12 is total & L1 is total & L2 is total )
by FDIFF_1:def 3;
reconsider L = L11 + L12 as LinearFunc by FDIFF_1:2;
reconsider R11 = ((SVF1 (3,f2,u0)) . z0) (#) R1, R12 = ((SVF1 (3,f1,u0)) . z0) (#) R2 as RestFunc by FDIFF_1:5;
reconsider R13 = R11 + R12 as RestFunc by FDIFF_1:4;
reconsider R14 = L1 (#) L2 as RestFunc by FDIFF_1:6;
reconsider R15 = R13 + R14, R17 = R1 (#) R2 as RestFunc by FDIFF_1:4;
reconsider R16 = R1 (#) L2, R18 = R2 (#) L1 as RestFunc by FDIFF_1:7;
reconsider R19 = R16 + R17 as RestFunc by FDIFF_1:4;
reconsider R20 = R19 + R18 as RestFunc by FDIFF_1:4;
reconsider R = R15 + R20 as RestFunc by FDIFF_1:4;
A11:
( 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 2;
A12:
N c= dom (SVF1 (3,f1,u0))
by A4, A9;
A13:
N c= dom (SVF1 (3,f2,u0))
by A7, A9;
A14:
for z being Real st z in N holds
z in dom (SVF1 (3,(f1 (#) f2),u0))
proof
let z be
Real;
( z in N implies z in dom (SVF1 (3,(f1 (#) f2),u0)) )
assume A15:
z in N
;
z in dom (SVF1 (3,(f1 (#) f2),u0))
then A16:
(
z in dom (reproj (3,u0)) &
(reproj (3,u0)) . z in dom f1 )
by A12, FUNCT_1:11;
(
z in dom (reproj (3,u0)) &
(reproj (3,u0)) . z in dom f2 )
by A13, A15, FUNCT_1:11;
then
(
z in dom (reproj (3,u0)) &
(reproj (3,u0)) . z in (dom f1) /\ (dom f2) )
by A16, XBOOLE_0:def 4;
then
(
z in dom (reproj (3,u0)) &
(reproj (3,u0)) . z in dom (f1 (#) f2) )
by VALUED_1:def 4;
hence
z in dom (SVF1 (3,(f1 (#) f2),u0))
by FUNCT_1:11;
verum
end;
then
for z being object st z in N holds
z in dom (SVF1 (3,(f1 (#) f2),u0))
;
then A17:
N c= dom (SVF1 (3,(f1 (#) f2),u0))
;
now for zz being Real st zz in N holds
((SVF1 (3,(f1 (#) f2),u0)) . zz) - ((SVF1 (3,(f1 (#) f2),u0)) . z0) = (L . (zz - z0)) + (R . (zz - z0))let zz be
Real;
( zz in N implies ((SVF1 (3,(f1 (#) f2),u0)) . zz) - ((SVF1 (3,(f1 (#) f2),u0)) . z0) = (L . (zz - z0)) + (R . (zz - z0)) )assume A18:
zz in N
;
((SVF1 (3,(f1 (#) f2),u0)) . zz) - ((SVF1 (3,(f1 (#) f2),u0)) . z0) = (L . (zz - z0)) + (R . (zz - z0))reconsider z =
zz,
zz0 =
z0 as
Element of
REAL by XREAL_0:def 1;
A19:
(((SVF1 (3,f1,u0)) . z) - ((SVF1 (3,f1,u0)) . z0)) + ((SVF1 (3,f1,u0)) . z0) = ((L1 . (z - z0)) + (R1 . (z - z0))) + ((SVF1 (3,f1,u0)) . z0)
by A5, A9, A18;
z in dom ((f1 (#) f2) * (reproj (3,u0)))
by A14, A18;
then A20:
(
z in dom (reproj (3,u0)) &
(reproj (3,u0)) . z in dom (f1 (#) f2) )
by FUNCT_1:11;
then
(reproj (3,u0)) . z in (dom f1) /\ (dom f2)
by VALUED_1:def 4;
then
(
(reproj (3,u0)) . z in dom f1 &
(reproj (3,u0)) . z in dom f2 )
by XBOOLE_0:def 4;
then A21:
(
z in dom (f1 * (reproj (3,u0))) &
z in dom (f2 * (reproj (3,u0))) )
by A20, FUNCT_1:11;
A22:
z0 in N
by RCOMP_1:16;
z0 in dom ((f1 (#) f2) * (reproj (3,u0)))
by A14, RCOMP_1:16;
then A23:
(
z0 in dom (reproj (3,u0)) &
(reproj (3,u0)) . z0 in dom (f1 (#) f2) )
by FUNCT_1:11;
then
(reproj (3,u0)) . z0 in (dom f1) /\ (dom f2)
by VALUED_1:def 4;
then
(
(reproj (3,u0)) . z0 in dom f1 &
(reproj (3,u0)) . z0 in dom f2 )
by XBOOLE_0:def 4;
then A24:
(
z0 in dom (f1 * (reproj (3,u0))) &
z0 in dom (f2 * (reproj (3,u0))) )
by A23, FUNCT_1:11;
thus ((SVF1 (3,(f1 (#) f2),u0)) . zz) - ((SVF1 (3,(f1 (#) f2),u0)) . z0) =
((f1 (#) f2) . ((reproj (3,u0)) . z)) - ((SVF1 (3,(f1 (#) f2),u0)) . z0)
by A17, A18, FUNCT_1:12
.=
((f1 . ((reproj (3,u0)) . z)) * (f2 . ((reproj (3,u0)) . z))) - ((SVF1 (3,(f1 (#) f2),u0)) . z0)
by VALUED_1:5
.=
(((SVF1 (3,f1,u0)) . z) * (f2 . ((reproj (3,u0)) . z))) - ((SVF1 (3,(f1 (#) f2),u0)) . z0)
by A21, FUNCT_1:12
.=
(((SVF1 (3,f1,u0)) . z) * ((SVF1 (3,f2,u0)) . z)) - (((f1 (#) f2) * (reproj (3,u0))) . z0)
by A21, FUNCT_1:12
.=
(((SVF1 (3,f1,u0)) . z) * ((SVF1 (3,f2,u0)) . z)) - ((f1 (#) f2) . ((reproj (3,u0)) . z0))
by A17, A22, FUNCT_1:12
.=
(((SVF1 (3,f1,u0)) . z) * ((SVF1 (3,f2,u0)) . z)) - ((f1 . ((reproj (3,u0)) . z0)) * (f2 . ((reproj (3,u0)) . z0)))
by VALUED_1:5
.=
(((SVF1 (3,f1,u0)) . z) * ((SVF1 (3,f2,u0)) . z)) - (((SVF1 (3,f1,u0)) . z0) * (f2 . ((reproj (3,u0)) . z0)))
by A24, FUNCT_1:12
.=
(((((SVF1 (3,f1,u0)) . z) * ((SVF1 (3,f2,u0)) . z)) + (- (((SVF1 (3,f1,u0)) . z) * ((SVF1 (3,f2,u0)) . z0)))) + (((SVF1 (3,f1,u0)) . z) * ((SVF1 (3,f2,u0)) . z0))) - (((SVF1 (3,f1,u0)) . z0) * ((SVF1 (3,f2,u0)) . z0))
by A24, FUNCT_1:12
.=
(((SVF1 (3,f1,u0)) . z) * (((SVF1 (3,f2,u0)) . z) - ((SVF1 (3,f2,u0)) . z0))) + ((((SVF1 (3,f1,u0)) . z) - ((SVF1 (3,f1,u0)) . z0)) * ((SVF1 (3,f2,u0)) . z0))
.=
(((SVF1 (3,f1,u0)) . z) * (((SVF1 (3,f2,u0)) . z) - ((SVF1 (3,f2,u0)) . z0))) + (((L1 . (z - z0)) + (R1 . (z - z0))) * ((SVF1 (3,f2,u0)) . z0))
by A5, A9, A18
.=
(((SVF1 (3,f1,u0)) . z) * (((SVF1 (3,f2,u0)) . z) - ((SVF1 (3,f2,u0)) . z0))) + ((((SVF1 (3,f2,u0)) . z0) * (L1 . (z - z0))) + (((SVF1 (3,f2,u0)) . z0) * (R1 . (z - z0))))
.=
(((SVF1 (3,f1,u0)) . z) * (((SVF1 (3,f2,u0)) . z) - ((SVF1 (3,f2,u0)) . z0))) + ((L11 . (z - z0)) + (((SVF1 (3,f2,u0)) . z0) * (R1 . (z - zz0))))
by A10, RFUNCT_1:57
.=
((((L1 . (z - z0)) + (R1 . (z - z0))) + ((SVF1 (3,f1,u0)) . z0)) * (((SVF1 (3,f2,u0)) . z) - ((SVF1 (3,f2,u0)) . z0))) + ((L11 . (z - z0)) + (R11 . (z - zz0)))
by A11, A19, RFUNCT_1:57
.=
((((L1 . (z - z0)) + (R1 . (z - z0))) + ((SVF1 (3,f1,u0)) . z0)) * ((L2 . (z - z0)) + (R2 . (z - z0)))) + ((L11 . (z - z0)) + (R11 . (z - z0)))
by A8, A9, A18
.=
((((L1 . (z - z0)) + (R1 . (z - z0))) * ((L2 . (z - z0)) + (R2 . (z - z0)))) + ((((SVF1 (3,f1,u0)) . z0) * (L2 . (z - z0))) + (((SVF1 (3,f1,u0)) . z0) * (R2 . (z - z0))))) + ((L11 . (z - z0)) + (R11 . (z - z0)))
.=
((((L1 . (z - z0)) + (R1 . (z - z0))) * ((L2 . (z - z0)) + (R2 . (z - zz0)))) + ((L12 . (z - z0)) + (((SVF1 (3,f1,u0)) . z0) * (R2 . (z - z0))))) + ((L11 . (z - z0)) + (R11 . (z - z0)))
by A10, RFUNCT_1:57
.=
((((L1 . (z - z0)) + (R1 . (z - z0))) * ((L2 . (z - z0)) + (R2 . (z - zz0)))) + ((L12 . (z - z0)) + (R12 . (z - z0)))) + ((L11 . (z - z0)) + (R11 . (z - z0)))
by A11, RFUNCT_1:57
.=
(((L1 . (z - z0)) + (R1 . (z - z0))) * ((L2 . (z - z0)) + (R2 . (z - z0)))) + ((L12 . (z - z0)) + ((L11 . (z - z0)) + ((R11 . (z - z0)) + (R12 . (z - z0)))))
.=
(((L1 . (z - z0)) + (R1 . (z - z0))) * ((L2 . (z - z0)) + (R2 . (z - zz0)))) + ((L12 . (z - z0)) + ((L11 . (z - z0)) + (R13 . (z - z0))))
by A11, RFUNCT_1:56
.=
(((L1 . (z - z0)) + (R1 . (z - z0))) * ((L2 . (z - z0)) + (R2 . (z - z0)))) + (((L11 . (z - z0)) + (L12 . (z - z0))) + (R13 . (z - z0)))
.=
((((L1 . (z - z0)) * (L2 . (z - z0))) + ((L1 . (z - z0)) * (R2 . (z - z0)))) + ((R1 . (z - zz0)) * ((L2 . (z - z0)) + (R2 . (z - z0))))) + ((L . (z - z0)) + (R13 . (z - z0)))
by A10, RFUNCT_1:56
.=
(((R14 . (z - z0)) + ((R2 . (z - z0)) * (L1 . (z - z0)))) + ((R1 . (z - z0)) * ((L2 . (z - z0)) + (R2 . (z - z0))))) + ((L . (z - z0)) + (R13 . (z - zz0)))
by A10, RFUNCT_1:56
.=
(((R14 . (z - z0)) + (R18 . (z - z0))) + (((R1 . (z - z0)) * (L2 . (z - z0))) + ((R1 . (z - z0)) * (R2 . (z - z0))))) + ((L . (z - z0)) + (R13 . (z - zz0)))
by A10, A11, RFUNCT_1:56
.=
(((R14 . (z - z0)) + (R18 . (z - z0))) + ((R16 . (z - z0)) + ((R1 . (z - z0)) * (R2 . (z - z0))))) + ((L . (z - z0)) + (R13 . (z - zz0)))
by A10, A11, RFUNCT_1:56
.=
(((R14 . (z - z0)) + (R18 . (z - z0))) + ((R16 . (z - z0)) + (R17 . (z - z0)))) + ((L . (z - z0)) + (R13 . (z - z0)))
by A11, RFUNCT_1:56
.=
(((R14 . (z - zz0)) + (R18 . (z - z0))) + (R19 . (z - z0))) + ((L . (z - z0)) + (R13 . (z - z0)))
by A11, RFUNCT_1:56
.=
((R14 . (z - z0)) + ((R19 . (z - z0)) + (R18 . (z - z0)))) + ((L . (z - z0)) + (R13 . (z - z0)))
.=
((L . (z - zz0)) + (R13 . (z - z0))) + ((R14 . (z - z0)) + (R20 . (z - z0)))
by A11, RFUNCT_1:56
.=
(L . (z - z0)) + (((R13 . (z - z0)) + (R14 . (z - z0))) + (R20 . (z - z0)))
.=
(L . (z - zz0)) + ((R15 . (z - z0)) + (R20 . (z - zz0)))
by A11, RFUNCT_1:56
.=
(L . (zz - z0)) + (R . (zz - z0))
by A11, RFUNCT_1:56
;
verum end;
hence
f1 (#) f2 is_partial_differentiable_in u0,3
by A3, A17, Th15; verum