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
A4: C = (cos + (<i> (#) sin)) | [.1,2.] ;
take C ; :: thesis: C is C1-curve-like
A5: dom (cos + (<i> (#) sin)) = REAL by FUNCT_2:def 1;
dom C = (dom (cos + (<i> (#) sin))) /\ [.1,2.] by A4, RELAT_1:90;
then A6: [.1,2.] = dom C by A5, XBOOLE_1:28;
A7: ].(- 5),5.[ is open by RCOMP_1:25;
A8: [.1,2.] c= ].(- 5),5.[ by XXREAL_1:47;
A9: cos is_differentiable_on ].(- 5),5.[ by A7, FDIFF_1:34, SIN_COS:72;
A10: sin is_differentiable_on ].(- 5),5.[ by A7, FDIFF_1:34, SIN_COS:73;
sin = sin | REAL

proof

A12: dom (sin | REAL) = (dom sin) /\ REAL by RELAT_1:90
.= REAL by SIN_COS:27 ;
for x0 being set st x0 in dom sin holds
sin . x0 = (sin | REAL) . x0 by FUNCT_1:72;
hence sin = sin | REAL by A12, SIN_COS:27, FUNCT_1:9; :: thesis: verum

end;

then sin | ].(- 5),5.[ is continuous by FCONT_1:17;
then (- sin) | ].(- 5),5.[ is continuous by SIN_COS:27, FCONT_1:22;
then A13: - (sin | ].(- 5),5.[) is continuous by RFUNCT_1:62;
A14: dom (- (sin | ].(- 5),5.[)) = dom ((- sin) | ].(- 5),5.[) by RFUNCT_1:62
.= (dom (- sin)) /\ ].(- 5),5.[ by RELAT_1:90
.= REAL /\ ].(- 5),5.[ by SIN_COS:27, VALUED_1:8
.= ].(- 5),5.[ by XBOOLE_1:28 ;
for x1 being Element of REAL st x1 in ].(- 5),5.[ holds
(- (sin | ].(- 5),5.[)) . x1 = diff (cos,x1)

proof

let x1 be Element of REAL ; :: thesis: ( x1 in ].(- 5),5.[ implies (- (sin | ].(- 5),5.[)) . x1 = diff (cos,x1) )
assume A15: x1 in ].(- 5),5.[ ; :: thesis: (- (sin | ].(- 5),5.[)) . x1 = diff (cos,x1)
A16: (- (sin | ].(- 5),5.[)) . x1 = ((- sin) | ].(- 5),5.[) . x1 by RFUNCT_1:62
.= (- sin) . x1 by A15, FUNCT_1:72
.= - (sin . x1) by RFUNCT_1:74
.= - ((sin | ].(- 5),5.[) . x1) by A15, FUNCT_1:72 ;
diff (cos,x1) = - (sin . x1) by SIN_COS:72
.= (- (sin | ].(- 5),5.[)) . x1 by A16, A15, FUNCT_1:72 ;
hence (- (sin | ].(- 5),5.[)) . x1 = diff (cos,x1) ; :: thesis: verum

end;

then A17: cos `| ].(- 5),5.[ is continuous by A9, A13, A14, FDIFF_1:def 8;
cos = cos | REAL

proof

A19: dom (cos | REAL) = (dom cos) /\ REAL by RELAT_1:90
.= REAL by SIN_COS:27 ;
for x0 being set st x0 in dom cos holds
cos . x0 = (cos | REAL) . x0 by FUNCT_1:72;
hence cos = cos | REAL by A19, SIN_COS:27, FUNCT_1:9; :: thesis: verum

end;

then A20: cos | ].(- 5),5.[ is continuous by FCONT_1:17;
A21: dom (cos | ].(- 5),5.[) = (dom cos) /\ ].(- 5),5.[ by RELAT_1:90
.= ].(- 5),5.[ by XBOOLE_1:28, SIN_COS:27 ;
for x1 being Element of REAL st x1 in ].(- 5),5.[ holds
(cos | ].(- 5),5.[) . x1 = diff (sin,x1)

proof

let x1 be Element of REAL ; :: thesis: ( x1 in ].(- 5),5.[ implies (cos | ].(- 5),5.[) . x1 = diff (sin,x1) )
assume A22: x1 in ].(- 5),5.[ ; :: thesis: (cos | ].(- 5),5.[) . x1 = diff (sin,x1)
diff (sin,x1) = cos . x1 by SIN_COS:73
.= (cos | ].(- 5),5.[) . x1 by A22, FUNCT_1:72 ;
hence (cos | ].(- 5),5.[) . x1 = diff (sin,x1) ; :: thesis: verum

end;

then sin `| ].(- 5),5.[ is continuous by A10, A20, A21, FDIFF_1:def 8;
hence C is C1-curve-like by A4, A6, A7, A8, A9, A10, A17, Def3, SIN_COS:27; :: thesis: verum