consider s being non empty finite Subset of NAT such that
A1: s = { (card t) where t is Element of the Sorts of (FreeEnv SCS) . v : verum } and
A2: size v,SCS = max s by CIRCUIT1:def 4;
size v,SCS in s by A2, XXREAL_2:def 8;
then consider e being Element of the Sorts of (FreeEnv SCS) . v such that
A3: size v,SCS = card e by A1;
reconsider SFv = the Sorts of (FreeEnv SCS) . v as non empty set ;
reconsider e' = e as Element of SFv ;
reconsider Fiev = (Fix_inp_ext iv) . v as Function of SFv,SFv ;
reconsider IT = Fiev . e' as Element of SFv ;
reconsider IT = IT as Element of the Sorts of (FreeEnv SCS) . v ;
take IT ; :: thesis: ex e being Element of the Sorts of (FreeEnv SCS) . v st
( card e = size v,SCS & IT = ((Fix_inp_ext iv) . v) . e )
take e ; :: thesis: ( card e = size v,SCS & IT = ((Fix_inp_ext iv) . v) . e )
thus card e = size v,SCS by A3; :: thesis: IT = ((Fix_inp_ext iv) . v) . e
thus IT = ((Fix_inp_ext iv) . v) . e ; :: thesis: verum