for x being ( ( real ) ( V11() real ext-real ) number ) st cos x : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) <> 0 : ( ( ) ( natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
cosec x : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = (sec x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / (tan x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

for x being ( ( real ) ( V11() real ext-real ) number ) st sin x : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) <> 0 : ( ( ) ( natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
cos x : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) = (sin x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) * (cot x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

for x1, x2, x3 being ( ( real ) ( V11() real ext-real ) number ) st sin x1 : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) <> 0 : ( ( ) ( natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) & sin x2 : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) <> 0 : ( ( ) ( natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) & sin x3 : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) <> 0 : ( ( ) ( natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
sin ((x1 : ( ( real ) ( V11() real ext-real ) number ) + x2 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) + x3 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) = (((sin x1 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) * (sin x2 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) * (sin x3 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) * (((((cot x2 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) * (cot x3 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) + ((cot x1 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) * (cot x3 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) + ((cot x1 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) * (cot x2 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) - 1 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

for x1, x2, x3 being ( ( real ) ( V11() real ext-real ) number ) st sin x1 : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) <> 0 : ( ( ) ( natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) & sin x2 : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) <> 0 : ( ( ) ( natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) & sin x3 : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) <> 0 : ( ( ) ( natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
cos ((x1 : ( ( real ) ( V11() real ext-real ) number ) + x2 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) + x3 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) = - ((((sin x1 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) * (sin x2 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) * (sin x3 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) * ((((cot x1 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) + (cot x2 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) + (cot x3 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) - (((cot x1 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) * (cot x2 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) * (cot x3 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

for x being ( ( real ) ( V11() real ext-real ) number ) holds sin (2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = (2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * (sin x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) * (cos x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

for x being ( ( real ) ( V11() real ext-real ) number ) st cos x : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) <> 0 : ( ( ) ( natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
sin (2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = (2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * (tan x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / (1 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + ((tan x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

for x being ( ( real ) ( V11() real ext-real ) number ) holds
( cos (2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = ((cos x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ^2) : ( ( ) ( V11() real ext-real ) set ) - ((sin x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ^2) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) & cos (2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = (2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * ((cos x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) - 1 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) & cos (2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = 1 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - (2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * ((sin x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) ;

for x being ( ( real ) ( V11() real ext-real ) number ) st cos x : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) <> 0 : ( ( ) ( natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
cos (2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = (1 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - ((tan x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / (1 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + ((tan x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

for x being ( ( real ) ( V11() real ext-real ) number ) st cos x : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) <> 0 : ( ( ) ( natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
tan (2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = (2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * (tan x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / (1 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - ((tan x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

for x being ( ( real ) ( V11() real ext-real ) number ) st sin x : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) <> 0 : ( ( ) ( natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
cot (2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = (((cot x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) - 1 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / (2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * (cot x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

for x being ( ( real ) ( V11() real ext-real ) number ) st cos x : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) <> 0 : ( ( ) ( natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
(sec x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2 : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = 1 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + ((tan x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

for x being ( ( real ) ( V11() real ext-real ) number ) holds cot x : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = 1 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) / (tan x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

for x being ( ( real ) ( V11() real ext-real ) number ) st cos x : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) <> 0 : ( ( ) ( natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) & sin x : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) <> 0 : ( ( ) ( natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
( sec (2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = ((sec x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / (1 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - ((tan x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) & sec (2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = ((cot x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) + (tan x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / ((cot x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) - (tan x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) ;

for x being ( ( real ) ( V11() real ext-real ) number ) st sin x : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) <> 0 : ( ( ) ( natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
(cosec x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2 : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = 1 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + ((cot x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

for x being ( ( real ) ( V11() real ext-real ) number ) st cos x : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) <> 0 : ( ( ) ( natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) & sin x : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) <> 0 : ( ( ) ( natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
( cosec (2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = ((sec x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) * (cosec x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / 2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) & cosec (2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = ((tan x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) + (cot x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / 2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) ;

for x being ( ( real ) ( V11() real ext-real ) number ) holds sin (3 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = (- (4 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * ((sin x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) |^ 3 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) + (3 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * (sin x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

for x being ( ( real ) ( V11() real ext-real ) number ) holds cos (3 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = (4 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * ((cos x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) |^ 3 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) - (3 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * (cos x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

for x being ( ( real ) ( V11() real ext-real ) number ) st cos x : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) <> 0 : ( ( ) ( natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
tan (3 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = ((3 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * (tan x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) - ((tan x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) |^ 3 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / (1 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - (3 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * ((tan x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

for x being ( ( real ) ( V11() real ext-real ) number ) st sin x : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) <> 0 : ( ( ) ( natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
cot (3 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = (((cot x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) |^ 3 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) - (3 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * (cot x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / ((3 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * ((cot x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) - 1 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

for x being ( ( real ) ( V11() real ext-real ) number ) holds (sin x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ^2 : ( ( ) ( V11() real ext-real ) set ) = (1 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - (cos (2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / 2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

for x being ( ( real ) ( V11() real ext-real ) number ) holds (cos x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ^2 : ( ( ) ( V11() real ext-real ) set ) = (1 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + (cos (2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / 2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

for x being ( ( real ) ( V11() real ext-real ) number ) holds (sin x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) |^ 3 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( V11() real ext-real ) set ) = ((3 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * (sin x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) - (sin (3 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / 4 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

for x being ( ( real ) ( V11() real ext-real ) number ) holds (cos x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) |^ 3 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( V11() real ext-real ) set ) = ((3 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * (cos x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) + (cos (3 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / 4 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

for x being ( ( real ) ( V11() real ext-real ) number ) holds (sin x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) |^ 4 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( V11() real ext-real ) set ) = ((3 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - (4 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * (cos (2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) + (cos (4 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / 8 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

for x being ( ( real ) ( V11() real ext-real ) number ) holds (cos x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) |^ 4 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( V11() real ext-real ) set ) = ((3 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + (4 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * (cos (2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) + (cos (4 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / 8 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

for x being ( ( real ) ( V11() real ext-real ) number ) holds
( sin (x : ( ( real ) ( V11() real ext-real ) number ) / 2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = sqrt ((1 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - (cos x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / 2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) or sin (x : ( ( real ) ( V11() real ext-real ) number ) / 2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = - (sqrt ((1 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - (cos x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / 2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) ;