let A, B, e be Real; :: thesis: ex f being Function of REAL,REAL st
for x being Real holds f . x = (A * (cos . (e * x))) + (B * (sin . (e * x)))
defpred S₁[ object , object ] means ex t being Real st
( $1 = t & $2 = (A * (cos . (e * t))) + (B * (sin . (e * t))) );
A0: for x being object st x in REAL holds
ex y being object st
( y in REAL & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in REAL implies ex y being object st
( y in REAL & S₁[x,y] ) )
assume x in REAL ; :: thesis: ex y being object st
( y in REAL & S₁[x,y] )
then reconsider t = x as Real ;
(A * (cos . (e * t))) + (B * (sin . (e * t))) in REAL by XREAL_0:def 1;
hence ex y being object st
( y in REAL & S₁[x,y] ) ; :: thesis: verum

end;

consider f being Function of REAL,REAL such that
A1: for x being object st x in REAL holds
S₁[x,f . x] from FUNCT_2:sch 1(A0);
take f ; :: thesis: for x being Real holds f . x = (A * (cos . (e * x))) + (B * (sin . (e * x)))
let x be Real; :: thesis: f . x = (A * (cos . (e * x))) + (B * (sin . (e * x)))
ex t being Real st
( x = t & f . x = (A * (cos . (e * t))) + (B * (sin . (e * t))) ) by XREAL_0:def 1, A1;
hence f . x = (A * (cos . (e * x))) + (B * (sin . (e * x))) ; :: thesis: verum