let z0 be Element of REAL 2; 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; ( 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
; f1 (#) f2 is_partial_differentiable_in z0,1
consider x0, y0 being Real such that
A3:
z0 = <*x0,y0*>
and
A4:
ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f1,z0)) & ex L being LinearFunc ex R being RestFunc 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, Th9;
reconsider x0 = x0, y0 = y0 as Element of REAL by XREAL_0:def 1;
consider N1 being Neighbourhood of x0 such that
A5:
N1 c= dom (SVF1 (1,f1,z0))
and
A6:
ex L being LinearFunc ex R being RestFunc 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 A4;
consider L1 being LinearFunc, R1 being RestFunc such that
A7:
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 A6;
consider x1, y1 being Real such that
A8:
z0 = <*x1,y1*>
and
A9:
ex N being Neighbourhood of x1 st
( N c= dom (SVF1 (1,f2,z0)) & ex L being LinearFunc ex R being RestFunc 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, Th9;
x0 = x1
by A3, A8, FINSEQ_1:77;
then consider N2 being Neighbourhood of x0 such that
A10:
N2 c= dom (SVF1 (1,f2,z0))
and
A11:
ex L being LinearFunc ex R being RestFunc 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 A9;
consider L2 being LinearFunc, R2 being RestFunc such that
A12:
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 A11;
consider N being Neighbourhood of x0 such that
A13:
N c= N1
and
A14:
N c= N2
by RCOMP_1:17;
A15:
N c= dom (SVF1 (1,f2,z0))
by A10, A14;
A16:
N c= dom (SVF1 (1,f1,z0))
by A5, A13;
A17:
for y being Real st y in N holds
y in dom (SVF1 (1,(f1 (#) f2),z0))
proof
let y be
Real;
( y in N implies y in dom (SVF1 (1,(f1 (#) f2),z0)) )
assume A18:
y in N
;
y in dom (SVF1 (1,(f1 (#) f2),z0))
then
(
(reproj (1,z0)) . y in dom f1 &
(reproj (1,z0)) . y in dom f2 )
by A16, A15, FUNCT_1:11;
then
(reproj (1,z0)) . y in (dom f1) /\ (dom f2)
by XBOOLE_0:def 4;
then A19:
(reproj (1,z0)) . y in dom (f1 (#) f2)
by VALUED_1:def 4;
y in dom (reproj (1,z0))
by A15, A18, FUNCT_1:11;
hence
y in dom (SVF1 (1,(f1 (#) f2),z0))
by A19, FUNCT_1:11;
verum
end;
then
for y being object st y in N holds
y in dom (SVF1 (1,(f1 (#) f2),z0))
;
then A20:
N c= dom (SVF1 (1,(f1 (#) f2),z0))
;
reconsider R12 = ((SVF1 (1,f1,z0)) . x0) (#) R2 as RestFunc by FDIFF_1:5;
A21:
L2 is total
by FDIFF_1:def 3;
reconsider R11 = ((SVF1 (1,f2,z0)) . x0) (#) R1 as RestFunc by FDIFF_1:5;
A22:
L1 is total
by FDIFF_1:def 3;
A23:
R1 is total
by FDIFF_1:def 2;
reconsider R17 = R1 (#) R2 as RestFunc by FDIFF_1:4;
reconsider R16 = R1 (#) L2, R18 = R2 (#) L1 as RestFunc by FDIFF_1:7;
reconsider R14 = L1 (#) L2 as RestFunc by FDIFF_1:6;
reconsider R19 = R16 + R17 as RestFunc by FDIFF_1:4;
reconsider R20 = R19 + R18 as RestFunc by FDIFF_1:4;
A24:
R14 is total
by FDIFF_1:def 2;
A25:
R18 is total
by FDIFF_1:def 2;
A26:
R2 is total
by FDIFF_1:def 2;
reconsider R13 = R11 + R12 as RestFunc by FDIFF_1:4;
reconsider L11 = ((SVF1 (1,f2,z0)) . x0) (#) L1, L12 = ((SVF1 (1,f1,z0)) . x0) (#) L2 as LinearFunc by FDIFF_1:3;
reconsider L = L11 + L12 as LinearFunc by FDIFF_1:2;
reconsider R15 = R13 + R14 as RestFunc by FDIFF_1:4;
reconsider R = R15 + R20 as RestFunc by FDIFF_1:4;
A27:
R16 is total
by FDIFF_1:def 2;
A28:
( L11 is total & L12 is total )
by FDIFF_1:def 3;
now for x being Real st x in N holds
((SVF1 (1,(f1 (#) f2),z0)) . x) - ((SVF1 (1,(f1 (#) f2),z0)) . x0) = (L . (x - x0)) + (R . (x - x0))A29:
x0 in dom ((f1 (#) f2) * (reproj (1,z0)))
by A17, RCOMP_1:16;
then A30:
x0 in dom (reproj (1,z0))
by FUNCT_1:11;
(reproj (1,z0)) . x0 in dom (f1 (#) f2)
by A29, FUNCT_1:11;
then A31:
(reproj (1,z0)) . x0 in (dom f1) /\ (dom f2)
by VALUED_1:def 4;
then
(reproj (1,z0)) . x0 in dom f1
by XBOOLE_0:def 4;
then A32:
x0 in dom (f1 * (reproj (1,z0)))
by A30, FUNCT_1:11;
(reproj (1,z0)) . x0 in dom f2
by A31, XBOOLE_0:def 4;
then A33:
x0 in dom (f2 * (reproj (1,z0)))
by A30, FUNCT_1:11;
let x be
Real;
( x in N implies ((SVF1 (1,(f1 (#) f2),z0)) . x) - ((SVF1 (1,(f1 (#) f2),z0)) . x0) = (L . (x - x0)) + (R . (x - x0)) )A34:
x0 in N
by RCOMP_1:16;
assume A35:
x in N
;
((SVF1 (1,(f1 (#) f2),z0)) . x) - ((SVF1 (1,(f1 (#) f2),z0)) . x0) = (L . (x - x0)) + (R . (x - x0))then A36:
(((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 A7, A13;
A37:
x in dom ((f1 (#) f2) * (reproj (1,z0)))
by A17, A35;
then A38:
x in dom (reproj (1,z0))
by FUNCT_1:11;
(reproj (1,z0)) . x in dom (f1 (#) f2)
by A37, FUNCT_1:11;
then A39:
(reproj (1,z0)) . x in (dom f1) /\ (dom f2)
by VALUED_1:def 4;
then
(reproj (1,z0)) . x in dom f1
by XBOOLE_0:def 4;
then A40:
x in dom (f1 * (reproj (1,z0)))
by A38, FUNCT_1:11;
reconsider xx0 =
x - x0 as
Element of
REAL by XREAL_0:def 1;
(reproj (1,z0)) . x in dom f2
by A39, XBOOLE_0:def 4;
then A41:
x in dom (f2 * (reproj (1,z0)))
by A38, FUNCT_1:11;
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 A20, A35, FUNCT_1:12
.=
((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 A40, FUNCT_1:12
.=
(((SVF1 (1,f1,z0)) . x) * ((SVF1 (1,f2,z0)) . x)) - (((f1 (#) f2) * (reproj (1,z0))) . x0)
by A41, FUNCT_1:12
.=
(((SVF1 (1,f1,z0)) . x) * ((SVF1 (1,f2,z0)) . x)) - ((f1 (#) f2) . ((reproj (1,z0)) . x0))
by A20, A34, FUNCT_1:12
.=
(((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 A32, FUNCT_1:12
.=
(((((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 A33, FUNCT_1:12
.=
(((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 A7, A13, A35
.=
(((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 . xx0)))
by A22, RFUNCT_1:57
.=
((((L1 . (x - x0)) + (R1 . xx0)) + ((SVF1 (1,f1,z0)) . x0)) * (((SVF1 (1,f2,z0)) . x) - ((SVF1 (1,f2,z0)) . x0))) + ((L11 . (x - x0)) + (R11 . (x - x0)))
by A23, A36, RFUNCT_1:57
.=
((((L1 . (x - x0)) + (R1 . (x - x0))) + ((SVF1 (1,f1,z0)) . x0)) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L11 . (x - x0)) + (R11 . (x - x0)))
by A12, A14, A35
.=
((((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 . xx0))
by A21, RFUNCT_1:57
.=
((((L1 . (x - x0)) + (R1 . xx0)) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L12 . (x - x0)) + (R12 . (x - x0)))) + ((L11 . (x - x0)) + (R11 . (x - x0)))
by A26, RFUNCT_1:57
.=
(((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 . xx0)) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L12 . (x - x0)) + ((L11 . (x - x0)) + (R13 . (x - x0))))
by A23, A26, RFUNCT_1:56
.=
(((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 . xx0) * (R2 . (x - x0)))) + ((R1 . (x - x0)) * ((L2 . (x - x0)) + (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . (x - x0)))
by A28, RFUNCT_1:56
.=
(((R14 . (x - x0)) + ((R2 . xx0) * (L1 . (x - x0)))) + ((R1 . (x - x0)) * ((L2 . (x - x0)) + (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . (x - x0)))
by A22, A21, RFUNCT_1:56
.=
(((R14 . (x - x0)) + (R18 . xx0)) + (((R1 . (x - x0)) * (L2 . (x - x0))) + ((R1 . (x - x0)) * (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . (x - x0)))
by A22, A26, RFUNCT_1:56
.=
(((R14 . (x - x0)) + (R18 . xx0)) + ((R16 . (x - x0)) + ((R1 . (x - x0)) * (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . (x - x0)))
by A21, A23, RFUNCT_1:56
.=
(((R14 . (x - x0)) + (R18 . xx0)) + ((R16 . (x - x0)) + (R17 . (x - x0)))) + ((L . (x - x0)) + (R13 . (x - x0)))
by A23, A26, RFUNCT_1:56
.=
(((R14 . (x - x0)) + (R18 . xx0)) + (R19 . (x - x0))) + ((L . (x - x0)) + (R13 . (x - x0)))
by A23, A26, A27, RFUNCT_1:56
.=
((R14 . (x - x0)) + ((R19 . (x - x0)) + (R18 . (x - x0)))) + ((L . (x - x0)) + (R13 . (x - x0)))
.=
((L . (x - x0)) + (R13 . xx0)) + ((R14 . (x - x0)) + (R20 . (x - x0)))
by A23, A26, A27, A25, RFUNCT_1:56
.=
(L . (x - x0)) + (((R13 . (x - x0)) + (R14 . (x - x0))) + (R20 . (x - x0)))
.=
(L . (x - x0)) + ((R15 . xx0) + (R20 . (x - x0)))
by A23, A26, A24, RFUNCT_1:56
.=
(L . (x - x0)) + (R . (x - x0))
by A23, A26, A24, A27, A25, RFUNCT_1:56
;
verum end;
hence
f1 (#) f2 is_partial_differentiable_in z0,1
by A3, A20, Th9; verum