set S = 1GateCircStr p,f;
set SORTS = the carrier of (1GateCircStr p,f) --> X;
set CHARACT = the carrier' of (1GateCircStr p,f) --> f;
A1: ( the carrier of (1GateCircStr p,f) = (rng p) \/ {[p,f]} & the carrier' of (1GateCircStr p,f) = {[p,f]} & the Arity of (1GateCircStr p,f) . [p,f] = p & the ResultSort of (1GateCircStr p,f) . [p,f] = [p,f] ) by Def6;
A2: [p,f] in {[p,f]} by TARSKI:def 1;
then [p,f] in the carrier of (1GateCircStr p,f) by A1, XBOOLE_0:def 3;
then A3: (the carrier of (1GateCircStr p,f) --> X) . [p,f] = X by FUNCOP_1:13;
A4: ( dom the Arity of (1GateCircStr p,f) = {[p,f]} & dom the ResultSort of (1GateCircStr p,f) = {[p,f]} ) by A1, FUNCT_2:def 1;
A5: len p = n by FINSEQ_1:def 18;
rng p c= the carrier of (1GateCircStr p,f) by A1, XBOOLE_1:7;
then p is FinSequence of the carrier of (1GateCircStr p,f) by FINSEQ_1:def 4;
then reconsider pp = p as Element of the carrier of (1GateCircStr p,f) * by FINSEQ_1:def 11;

now

let i be set ; :: thesis: ( i in the carrier' of (1GateCircStr p,f) implies (the carrier' of (1GateCircStr p,f) --> f) . i is Function of ((((the carrier of (1GateCircStr p,f) --> X) # ) * the Arity of (1GateCircStr p,f)) . i),(((the carrier of (1GateCircStr p,f) --> X) * the ResultSort of (1GateCircStr p,f)) . i) )
assume A6: i in the carrier' of (1GateCircStr p,f) ; :: thesis: (the carrier' of (1GateCircStr p,f) --> f) . i is Function of ((((the carrier of (1GateCircStr p,f) --> X) # ) * the Arity of (1GateCircStr p,f)) . i),(((the carrier of (1GateCircStr p,f) --> X) * the ResultSort of (1GateCircStr p,f)) . i)
then i = [p,f] by A1, TARSKI:def 1;
then ( (the carrier' of (1GateCircStr p,f) --> f) . i = f & (((the carrier of (1GateCircStr p,f) --> X) # ) * the Arity of (1GateCircStr p,f)) . i = ((the carrier of (1GateCircStr p,f) --> X) # ) . p & ((the carrier of (1GateCircStr p,f) --> X) # ) . pp = n -tuples_on X & ((the carrier of (1GateCircStr p,f) --> X) * the ResultSort of (1GateCircStr p,f)) . i = X ) by A1, A3, A4, A5, A6, Th6, FUNCOP_1:13, FUNCT_1:23;
hence (the carrier' of (1GateCircStr p,f) --> f) . i is Function of ((((the carrier of (1GateCircStr p,f) --> X) # ) * the Arity of (1GateCircStr p,f)) . i),(((the carrier of (1GateCircStr p,f) --> X) * the ResultSort of (1GateCircStr p,f)) . i) ; :: thesis: verum

end;

then reconsider CHARACT = the carrier' of (1GateCircStr p,f) --> f as ManySortedFunction of ((the carrier of (1GateCircStr p,f) --> X) # ) * the Arity of (1GateCircStr p,f),(the carrier of (1GateCircStr p,f) --> X) * the ResultSort of (1GateCircStr p,f) by PBOOLE:def 18;
reconsider A = MSAlgebra(# (the carrier of (1GateCircStr p,f) --> X),CHARACT #) as strict non-empty MSAlgebra of 1GateCircStr p,f by MSUALG_1:def 8;
take A ; :: thesis: ( the Sorts of A = the carrier of (1GateCircStr p,f) --> X & the Charact of A . [p,f] = f )
thus ( the Sorts of A = the carrier of (1GateCircStr p,f) --> X & the Charact of A . [p,f] = f ) by A1, A2, FUNCOP_1:13; :: thesis: verum