defpred S₁[ set , set ] means ex g being Gate of (X -CircuitStr ) st
( g = $1 & $2 = the_action_of g,A );

A4: now

let x be set ; :: thesis: ( x in the carrier' of (X -CircuitStr ) implies ex y being set st S₁[x,y] )
assume x in the carrier' of (X -CircuitStr ) ; :: thesis: ex y being set st S₁[x,y]
then reconsider g = x as Gate of (X -CircuitStr ) ;
reconsider y = the_action_of g,A as set ;
take y = y; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

consider CHARACT being ManySortedSet of the carrier' of (X -CircuitStr ) such that
A5: for x being set st x in the carrier' of (X -CircuitStr ) holds
S₁[x,CHARACT . x] from PBOOLE:sch 3(A4);
A6: dom CHARACT = the carrier' of (X -CircuitStr ) by PARTFUN1:def 4;
CHARACT is Function-yielding

proof

let x be set ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 CHARACT or CHARACT . x is set )
assume x in dom CHARACT ; :: thesis: CHARACT . x is set
then ex g being Gate of (X -CircuitStr ) st
( g = x & CHARACT . x = the_action_of g,A ) by A5, A6;
hence CHARACT . x is set ; :: thesis: verum

end;

then reconsider CHARACT = CHARACT as ManySortedFunction of the carrier' of (X -CircuitStr ) ;
CHARACT is ManySortedFunction of ((X -CircuitSorts A) # ) * the Arity of (X -CircuitStr ),(X -CircuitSorts A) * the ResultSort of (X -CircuitStr )

proof

let i be set ; :: according to PBOOLE:def 18 :: thesis: ( not i in the carrier' of (X -CircuitStr ) or CHARACT . i is Element of bool [:((((X -CircuitSorts A) # ) * the Arity of (X -CircuitStr )) . i),(((X -CircuitSorts A) * the ResultSort of (X -CircuitStr )) . i):] )
assume A7: i in the carrier' of (X -CircuitStr ) ; :: thesis: CHARACT . i is Element of bool [:((((X -CircuitSorts A) # ) * the Arity of (X -CircuitStr )) . i),(((X -CircuitSorts A) * the ResultSort of (X -CircuitStr )) . i):]
then not X -CircuitStr is void ;
then reconsider X9 = X as SetWithCompoundTerm of S,V by Th3;
reconsider g = i as Gate of (X9 -CircuitStr ) by A7;
A8: the_result_sort_of g = g by FUNCT_1:35;
then reconsider v = g as Vertex of (X9 -CircuitStr ) ;
reconsider I = i as CompoundTerm of S,V by A7, Th4;
I . {} in [:the carrier' of S,{the carrier of S}:] by MSATERM:def 6;
then consider o, y being set such that
A9: o in the carrier' of S and
A10: y in {the carrier of S} and
A11: I . {} = [o,y] by ZFMISC_1:103;
reconsider o = o as OperSymbol of S by A9;
A12: o = (I . {} ) `1 by A11, MCART_1:7;
A13: y = the carrier of S by A10, TARSKI:def 1;
ex g being Gate of (X -CircuitStr ) st
( g = i & CHARACT . i = the_action_of g,A ) by A5, A7;
then A14: CHARACT . i = the_action_of g,A
.= the Charact of A . o by A12, Def3 ;
A15: (the Sorts of A * the ResultSort of S) . o = the Sorts of A . (the_result_sort_of o) by FUNCT_2:21
.= the Sorts of A . (the_sort_of I) by A11, A13, MSATERM:17 ;
A16: ((X -CircuitSorts A) * the ResultSort of (X -CircuitStr )) . g = (X -CircuitSorts A) . (the_result_sort_of g) by FUNCT_2:21
.= the_sort_of v,A by A8, Def4
.= the Sorts of A . (the_sort_of I) by Def2 ;
A17: (((X -CircuitSorts A) # ) * the Arity of (X -CircuitStr )) . g = ((X -CircuitSorts A) # ) . (the_arity_of g) by FUNCT_2:21
.= product ((X9 -CircuitSorts A) * (the_arity_of g)) by PBOOLE:def 19
.= product (the Sorts of A * (the_arity_of o)) by A11, A13, Th14 ;
((the Sorts of A # ) * the Arity of S) . o = (the Sorts of A # ) . (the_arity_of o) by FUNCT_2:21
.= product (the Sorts of A * (the_arity_of o)) by PBOOLE:def 19 ;
hence CHARACT . i is Element of bool [:((((X -CircuitSorts A) # ) * the Arity of (X -CircuitStr )) . i),(((X -CircuitSorts A) * the ResultSort of (X -CircuitStr )) . i):] by A14, A15, A16, A17, PBOOLE:def 18; :: thesis: verum

end;

then reconsider CHARACT = CHARACT as ManySortedFunction of ((X -CircuitSorts A) # ) * the Arity of (X -CircuitStr ),(X -CircuitSorts A) * the ResultSort of (X -CircuitStr ) ;
take CHARACT ; :: thesis: for g being Gate of (X -CircuitStr ) st g in the carrier' of (X -CircuitStr ) holds
CHARACT . g = the_action_of g,A
let g be Gate of (X -CircuitStr ); :: thesis: ( g in the carrier' of (X -CircuitStr ) implies CHARACT . g = the_action_of g,A )
assume g in the carrier' of (X -CircuitStr ) ; :: thesis: CHARACT . g = the_action_of g,A
then ex h being Gate of (X -CircuitStr ) st
( h = g & CHARACT . g = the_action_of h,A ) by A5;
hence CHARACT . g = the_action_of g,A ; :: thesis: verum