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 ; :: thesis: 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; :: thesis: ( x1 in ].(- 5),5.[ implies (- (sin | ].(- 5),5.[)) . x1 = diff (cos,x1) )
assume A10: x1 in ].(- 5),5.[ ; :: thesis: (- (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) ; :: thesis: 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; :: thesis: ( x1 in ].(- 5),5.[ implies (cos | ].(- 5),5.[) . x1 = diff (sin,x1) )
assume A15: x1 in ].(- 5),5.[ ; :: thesis: (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) ; :: thesis: 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; :: thesis: verum