set S = 1GateCircStr p,f,x;
set g1 = (rng p) --> X;
set g2 = x .--> Y;
set SORTS = ((rng p) --> X) +* (x .--> Y);
set CHARACT = the carrier' of (1GateCircStr p,f,x) --> f;
A2: ( the carrier of (1GateCircStr p,f,x) = (rng p) \/ {x} & the carrier' of (1GateCircStr p,f,x) = {[p,f]} & the Arity of (1GateCircStr p,f,x) . [p,f] = p & the ResultSort of (1GateCircStr p,f,x) . [p,f] = x ) by Def5;
A3: ( x in {x} & dom (x .--> Y) = {x} & dom ((rng p) --> X) = rng p ) by FUNCOP_1:19, TARSKI:def 1;
then A4: (((rng p) --> X) +* (x .--> Y)) . x = (x .--> Y) . x by FUNCT_4:14
.= Y by A3, FUNCOP_1:13 ;
reconsider SORTS = ((rng p) --> X) +* (x .--> Y) as V2() ManySortedSet of by A2;
A5: ( dom the Arity of (1GateCircStr p,f,x) = {[p,f]} & dom the ResultSort of (1GateCircStr p,f,x) = {[p,f]} ) by A2, FUNCT_2:def 1;
A6: len p = n by FINSEQ_1:def 18;
rng p c= the carrier of (1GateCircStr p,f,x) by A2, XBOOLE_1:7;
then p is FinSequence of the carrier of (1GateCircStr p,f,x) by FINSEQ_1:def 4;
then reconsider pp = p as Element of the carrier of (1GateCircStr p,f,x) * by FINSEQ_1:def 11;
p is FinSequence of rng p by FINSEQ_1:def 4;
then reconsider p' = p as Element of (rng p) * by FINSEQ_1:def 11;
(rng p) --> X tolerates x .--> Y

proof

let y be set ; :: according to PARTFUN1:def 6 :: thesis: ( not y in (dom ((rng p) --> X)) /\ (dom (x .--> Y)) or ((rng p) --> X) . y = (x .--> Y) . y )
assume A7: y in (dom ((rng p) --> X)) /\ (dom (x .--> Y)) ; :: thesis: ((rng p) --> X) . y = (x .--> Y) . y
then ( y in {x} & y in rng p ) by A3, XBOOLE_0:def 4;
then ( x = y & ((rng p) --> X) . y = X & (x .--> Y) . y = Y ) by FUNCOP_1:13, TARSKI:def 1;
hence ((rng p) --> X) . y = (x .--> Y) . y by A1, A3, A7, XBOOLE_0:def 4; :: thesis: verum

end;

then (rng p) --> X c= SORTS by FUNCT_4:29;
then ( ((rng p) --> X) # c= SORTS # & dom (((rng p) --> X) # ) = (rng p) * ) by Th3, PARTFUN1:def 4;
then A8: (((rng p) --> X) # ) . p' = (SORTS # ) . pp by GRFUNC_1:8;

now

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

end;

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