set a = 1;
set b = 2;
set x = cos ;
set y = sin ;
set Z = ].(- 5),5.[;
consider C being PartFunc of REAL,COMPLEX such that
A1:
C = (cos + (<i> (#) sin)) | [.1,2.]
;
take
C
; C is C1-curve-like
A2:
dom (cos + (<i> (#) sin)) = REAL
by FUNCT_2:def 1;
dom C = (dom (cos + (<i> (#) sin))) /\ [.1,2.]
by A1, RELAT_1:61;
then A3:
[.1,2.] = dom C
by A2, XBOOLE_1:28;
A4:
].(- 5),5.[ is open
by RCOMP_1:7;
A5:
[.1,2.] c= ].(- 5),5.[
by XXREAL_1:47;
A6:
cos is_differentiable_on ].(- 5),5.[
by A4, FDIFF_1:26, SIN_COS:67;
A7:
sin is_differentiable_on ].(- 5),5.[
by A4, FDIFF_1:26, SIN_COS:68;
sin = sin | REAL
;
then
sin | ].(- 5),5.[ is continuous
by FCONT_1:16;
then
(- sin) | ].(- 5),5.[ is continuous
by FCONT_1:21, SIN_COS:24;
then A8:
- (sin | ].(- 5),5.[) is continuous
by RFUNCT_1:46;
A9: dom (- (sin | ].(- 5),5.[)) =
dom ((- sin) | ].(- 5),5.[)
by RFUNCT_1:46
.=
(dom (- sin)) /\ ].(- 5),5.[
by RELAT_1:61
.=
REAL /\ ].(- 5),5.[
by SIN_COS:24, VALUED_1:8
.=
].(- 5),5.[
by XBOOLE_1:28
;
for x1 being Real st x1 in ].(- 5),5.[ holds
(- (sin | ].(- 5),5.[)) . x1 = diff (cos,x1)
proof
let x1 be
Real;
( x1 in ].(- 5),5.[ implies (- (sin | ].(- 5),5.[)) . x1 = diff (cos,x1) )
assume A10:
x1 in ].(- 5),5.[
;
(- (sin | ].(- 5),5.[)) . x1 = diff (cos,x1)
reconsider x1 =
x1 as
Element of
REAL by XREAL_0:def 1;
A11:
(- (sin | ].(- 5),5.[)) . x1 =
((- sin) | ].(- 5),5.[) . x1
by RFUNCT_1:46
.=
(- sin) . x1
by A10, FUNCT_1:49
.=
- (sin . x1)
by RFUNCT_1:58
.=
- ((sin | ].(- 5),5.[) . x1)
by A10, FUNCT_1:49
;
diff (
cos,
x1) =
- (sin . x1)
by SIN_COS:67
.=
(- (sin | ].(- 5),5.[)) . x1
by A11, A10, FUNCT_1:49
;
hence
(- (sin | ].(- 5),5.[)) . x1 = diff (
cos,
x1)
;
verum
end;
then A12:
cos `| ].(- 5),5.[ is continuous
by A6, A8, A9, FDIFF_1:def 7;
cos = cos | REAL
;
then A13:
cos | ].(- 5),5.[ is continuous
by FCONT_1:16;
A14: dom (cos | ].(- 5),5.[) =
(dom cos) /\ ].(- 5),5.[
by RELAT_1:61
.=
].(- 5),5.[
by SIN_COS:24, XBOOLE_1:28
;
for x1 being Real st x1 in ].(- 5),5.[ holds
(cos | ].(- 5),5.[) . x1 = diff (sin,x1)
proof
let x1 be
Real;
( x1 in ].(- 5),5.[ implies (cos | ].(- 5),5.[) . x1 = diff (sin,x1) )
assume A15:
x1 in ].(- 5),5.[
;
(cos | ].(- 5),5.[) . x1 = diff (sin,x1)
diff (
sin,
x1) =
cos . x1
by SIN_COS:68
.=
(cos | ].(- 5),5.[) . x1
by A15, FUNCT_1:49
;
hence
(cos | ].(- 5),5.[) . x1 = diff (
sin,
x1)
;
verum
end;
then
sin `| ].(- 5),5.[ is continuous
by A7, A13, A14, FDIFF_1:def 7;
hence
C is C1-curve-like
by A1, A3, A4, A5, A6, A7, A12, SIN_COS:24; verum