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

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