reconsider SFv = the Sorts of (FreeEnv SCS) . v as non empty set ;
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 Fiev = (Fix_inp_ext iv) . v as Function of SFv,SFv ;
reconsider e9 = e as Element of SFv ;
reconsider IT = Fiev . e9 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