theorem Th20: :: NOMIN_7:20

for V, A being set
for z being Element of V
for loc being b₁ -valued Function
for n0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & ( for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ) holds
PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Fibonacci_inv (A,loc,n0))) ||= SC_Psuperpos ((valid_Fibonacci_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z)