set S = 1GateCircStr (p,f);
set SORTS = the carrier of (1GateCircStr (p,f)) --> X;
set CHARACT = the carrier' of (1GateCircStr (p,f)) --> f;
A1: len p = n by CARD_1:def 7;
A2: the Arity of (1GateCircStr (p,f)) . [p,f] = p by Def6;
A3: the ResultSort of (1GateCircStr (p,f)) . [p,f] = [p,f] by Def6;
A4: the carrier' of (1GateCircStr (p,f)) = {[p,f]} by Def6;
then A5: dom the ResultSort of (1GateCircStr (p,f)) = {[p,f]} by FUNCT_2:def 1;
A6: the carrier of (1GateCircStr (p,f)) = (rng p) \/ {[p,f]} by Def6;
then rng p c= the carrier of (1GateCircStr (p,f)) by 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;
A7: [p,f] in {[p,f]} by TARSKI:def 1;
then [p,f] in the carrier of (1GateCircStr (p,f)) by A6, XBOOLE_0:def 3;
then A8: ( the carrier of (1GateCircStr (p,f)) --> X) . [p,f] = X by FUNCOP_1:7;
A9: dom the Arity of (1GateCircStr (p,f)) = {[p,f]} by A4, FUNCT_2:def 1;

now :: thesis: for i being object st i in the carrier' of (1GateCircStr (p,f)) holds
( 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)

let i be object ; :: 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) )
A10: (( the carrier of (1GateCircStr (p,f)) --> X) #) . pp = n -tuples_on X by A1, Th2;
assume A11: 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 A12: i = [p,f] by A4, TARSKI:def 1;
then A13: ((( the carrier of (1GateCircStr (p,f)) --> X) #) * the Arity of (1GateCircStr (p,f))) . i = (( the carrier of (1GateCircStr (p,f)) --> X) #) . p by A4, A2, A9, A11, FUNCT_1:13;
(( the carrier of (1GateCircStr (p,f)) --> X) * the ResultSort of (1GateCircStr (p,f))) . i = X by A4, A3, A8, A5, A11, A12, FUNCT_1:13;
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) by A11, A13, A10, FUNCOP_1:7; :: 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 15;
reconsider A = MSAlgebra(# ( the carrier of (1GateCircStr (p,f)) --> X),CHARACT #) as strict non-empty MSAlgebra over 1GateCircStr (p,f) by MSUALG_1:def 3;
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 A4, A7, FUNCOP_1:7; :: thesis: verum