let h, x be Real; :: thesis: ( x in dom tan & x - h in dom tan implies (bD (((tan (#) tan) (#) sin),h)) . x = (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - (((sin . (x - h)) |^ 3) * (((cos . (x - h)) ") |^ 2)) )
set f = (tan (#) tan) (#) sin;
assume A1: ( x in dom tan & x - h in dom tan ) ; :: thesis: (bD (((tan (#) tan) (#) sin),h)) . x = (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - (((sin . (x - h)) |^ 3) * (((cos . (x - h)) ") |^ 2))
( x in dom ((tan (#) tan) (#) sin) & x - h in dom ((tan (#) tan) (#) sin) )

proof

set f1 = tan (#) tan;
set f2 = sin ;
A2: ( x in dom (tan (#) tan) & x - h in dom (tan (#) tan) )

proof

( x in (dom tan) /\ (dom tan) & x - h in (dom tan) /\ (dom tan) ) by A1;
hence ( x in dom (tan (#) tan) & x - h in dom (tan (#) tan) ) by VALUED_1:def 4; :: thesis: verum

end;

( x in (dom (tan (#) tan)) /\ (dom sin) & x - h in (dom (tan (#) tan)) /\ (dom sin) ) by A2, SIN_COS:24, XBOOLE_0:def 4;
hence ( x in dom ((tan (#) tan) (#) sin) & x - h in dom ((tan (#) tan) (#) sin) ) by VALUED_1:def 4; :: thesis: verum

end;

then (bD (((tan (#) tan) (#) sin),h)) . x = (((tan (#) tan) (#) sin) . x) - (((tan (#) tan) (#) sin) . (x - h)) by DIFF_1:38
.= (((tan (#) tan) . x) * (sin . x)) - (((tan (#) tan) (#) sin) . (x - h)) by VALUED_1:5
.= (((tan (#) tan) . x) * (sin . x)) - (((tan (#) tan) . (x - h)) * (sin . (x - h))) by VALUED_1:5
.= (((tan . x) * (tan . x)) * (sin . x)) - (((tan (#) tan) . (x - h)) * (sin . (x - h))) by VALUED_1:5
.= (((tan . x) * (tan . x)) * (sin . x)) - (((tan . (x - h)) * (tan . (x - h))) * (sin . (x - h))) by VALUED_1:5
.= ((((sin . x) * ((cos . x) ")) * (tan . x)) * (sin . x)) - (((tan . (x - h)) * (tan . (x - h))) * (sin . (x - h))) by A1, RFUNCT_1:def 1
.= ((((sin . x) * ((cos . x) ")) * ((sin . x) * ((cos . x) "))) * (sin . x)) - (((tan . (x - h)) * (tan . (x - h))) * (sin . (x - h))) by A1, RFUNCT_1:def 1
.= ((((sin . x) * ((cos . x) ")) * ((sin . x) * ((cos . x) "))) * (sin . x)) - ((((sin . (x - h)) * ((cos . (x - h)) ")) * (tan . (x - h))) * (sin . (x - h))) by A1, RFUNCT_1:def 1
.= ((((sin . x) * ((cos . x) ")) * ((sin . x) * ((cos . x) "))) * (sin . x)) - ((((sin . (x - h)) * ((cos . (x - h)) ")) * ((sin . (x - h)) * ((cos . (x - h)) "))) * (sin . (x - h))) by A1, RFUNCT_1:def 1
.= ((((sin . x) * (sin . x)) * (sin . x)) * (((cos . x) ") * ((cos . x) "))) - ((((sin . (x - h)) * (sin . (x - h))) * (sin . (x - h))) * (((cos . (x - h)) ") * ((cos . (x - h)) ")))
.= (((((sin . x) |^ 1) * (sin . x)) * (sin . x)) * (((cos . x) ") * ((cos . x) "))) - ((((sin . (x - h)) * (sin . (x - h))) * (sin . (x - h))) * (((cos . (x - h)) ") * ((cos . (x - h)) ")))
.= ((((sin . x) |^ (1 + 1)) * (sin . x)) * (((cos . x) ") * ((cos . x) "))) - ((((sin . (x - h)) * (sin . (x - h))) * (sin . (x - h))) * (((cos . (x - h)) ") * ((cos . (x - h)) "))) by NEWTON:6
.= (((sin . x) |^ (2 + 1)) * (((cos . x) ") * ((cos . x) "))) - ((((sin . (x - h)) * (sin . (x - h))) * (sin . (x - h))) * (((cos . (x - h)) ") * ((cos . (x - h)) "))) by NEWTON:6
.= (((sin . x) |^ 3) * ((((cos . x) ") |^ 1) * ((cos . x) "))) - ((((sin . (x - h)) * (sin . (x - h))) * (sin . (x - h))) * (((cos . (x - h)) ") * ((cos . (x - h)) ")))
.= (((sin . x) |^ 3) * (((cos . x) ") |^ (1 + 1))) - ((((sin . (x - h)) * (sin . (x - h))) * (sin . (x - h))) * (((cos . (x - h)) ") * ((cos . (x - h)) "))) by NEWTON:6
.= (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - (((((sin . (x - h)) |^ 1) * (sin . (x - h))) * (sin . (x - h))) * (((cos . (x - h)) ") * ((cos . (x - h)) ")))
.= (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - ((((sin . (x - h)) |^ (1 + 1)) * (sin . (x - h))) * (((cos . (x - h)) ") * ((cos . (x - h)) "))) by NEWTON:6
.= (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - (((sin . (x - h)) |^ (2 + 1)) * (((cos . (x - h)) ") * ((cos . (x - h)) "))) by NEWTON:6
.= (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - (((sin . (x - h)) |^ 3) * ((((cos . (x - h)) ") |^ 1) * ((cos . (x - h)) ")))
.= (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - (((sin . (x - h)) |^ 3) * (((cos . (x - h)) ") |^ (1 + 1))) by NEWTON:6
.= (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - (((sin . (x - h)) |^ 3) * (((cos . (x - h)) ") |^ 2)) ;
hence (bD (((tan (#) tan) (#) sin),h)) . x = (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - (((sin . (x - h)) |^ 3) * (((cos . (x - h)) ") |^ 2)) ; :: thesis: verum