let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis: for A being non-empty Circuit of IIG
for iv being InputValues of A
for v being Vertex of IIG
for e, e1 being Element of the Sorts of (FreeEnv A) . v st e1 = ((Fix_inp_ext iv) . v) . e holds
card e = card e1
let A be non-empty Circuit of IIG; :: thesis: for iv being InputValues of A
for v being Vertex of IIG
for e, e1 being Element of the Sorts of (FreeEnv A) . v st e1 = ((Fix_inp_ext iv) . v) . e holds
card e = card e1
let iv be InputValues of A; :: thesis: for v being Vertex of IIG
for e, e1 being Element of the Sorts of (FreeEnv A) . v st e1 = ((Fix_inp_ext iv) . v) . e holds
card e = card e1
let v be Vertex of IIG; :: thesis: for e, e1 being Element of the Sorts of (FreeEnv A) . v st e1 = ((Fix_inp_ext iv) . v) . e holds
card e = card e1
let e, e1 be Element of the Sorts of (FreeEnv A) . v; :: thesis: ( e1 = ((Fix_inp_ext iv) . v) . e implies card e = card e1 )
assume e1 = ((Fix_inp_ext iv) . v) . e ; :: thesis: card e = card e1
then dom e = dom e1 by Th6;
hence card e = card (dom e1) by CARD_1:62
.= card e1 by CARD_1:62 ;
:: thesis: verum