theorem Th18: :: NOMIN_7:18

for V, A being set
for loc being b₁ -valued Function
for n0 being Nat st not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & ( for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 2 is_a_value_on T & loc /. 4 is_a_value_on T & loc /. 6 is_a_value_on T ) ) & Seg 6 c= dom loc & loc | (Seg 6) is one-to-one holds
<*(Fibonacci_inv (A,loc,n0)),(Fibonacci_main_loop (A,loc)),(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Fibonacci_inv (A,loc,n0))))*> is SFHT of (ND (V,A))