deffunc H₁( Nat, State of SCS) -> State of SCS = Following ($2,(($1 + 1) -th_InputValues InpFs));
thus ( ex IT being sequence of (product the Sorts of SCS) st
( IT . 0 = InitialComp (s,InpFs) & ( for i being Nat holds IT . (i + 1) = H₁(i,IT . i) ) ) & ( for IT1, IT2 being sequence of (product the Sorts of SCS) st IT1 . 0 = InitialComp (s,InpFs) & ( for i being Nat holds IT1 . (i + 1) = H₁(i,IT1 . i) ) & IT2 . 0 = InitialComp (s,InpFs) & ( for i being Nat holds IT2 . (i + 1) = H₁(i,IT2 . i) ) holds
IT1 = IT2 ) ) from PRE_CIRC:sch 3(); :: thesis: verum