:: Preliminaries to Circuits, I :: by Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec and Pauline N. Kawamoto :: :: Received November 17, 1994 :: Copyright (c) 1994-2012 Association of Mizar Users
::---------------------------------------------------------------------------
:: Many Sorted Sets and Functions
::---------------------------------------------------------------------------
ex f being ManySortedSet of F1() st for i being Element of F1() st i in F1() holds ( ( P1[i] implies f . i = F2(i) ) & ( P1[i] implies f . i = F3(i) ) )
( ex f being Function of NAT,F1() st ( f .0= F2() & ( for i being Nat holds f .(i + 1)= F3(i,(f . i)) ) ) & ( for f1, f2 being Function of NAT,F1() st f1 .0= F2() & ( for i being Nat holds f1 .(i + 1)= F3(i,(f1 . i)) ) & f2 .0= F2() & ( for i being Nat holds f2 .(i + 1)= F3(i,(f2 . i)) ) holds f1 = f2 ) )
:: Many Sorted Sets and Functions
::---------------------------------------------------------------------------