p is FinSequence of rng p by FINSEQ_1:def 4;
then reconsider p9 = p as Element of (rng p) * by FINSEQ_1:def 11;
set g1 = (rng p) --> X;
set g2 = x .--> Y;
set S = 1GateCircStr p,f,x;
set SORTS = ((rng p) --> X) +* (x .--> Y);
set CHARACT = the carrier' of (1GateCircStr p,f,x) --> f;
A2: dom (x .--> Y) = {x} by FUNCOP_1:19;
A3: x in {x} by TARSKI:def 1;
then A4: (((rng p) --> X) +* (x .--> Y)) . x = (x .--> Y) . x by A2, FUNCT_4:14
.= Y by A3, FUNCOP_1:13 ;
A5: the carrier of (1GateCircStr p,f,x) = (rng p) \/ {x} by Def5;
then reconsider SORTS = ((rng p) --> X) +* (x .--> Y) as V2() ManySortedSet of the carrier of (1GateCircStr p,f,x) ;
rng p c= the carrier of (1GateCircStr p,f,x) by A5, 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;
A6: dom (((rng p) --> X) # ) = (rng p) * by PARTFUN1:def 4;
A7: dom ((rng p) --> X) = rng p by FUNCOP_1:19;
(rng p) --> X tolerates x .--> Y

proof

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

end;

then (rng p) --> X c= SORTS by FUNCT_4:29;
then ((rng p) --> X) # c= SORTS # by Th3;
then A11: (((rng p) --> X) # ) . p9 = (SORTS # ) . pp by A6, GRFUNC_1:8;
A12: the carrier' of (1GateCircStr p,f,x) = {[p,f]} by Def5;
then A13: dom the ResultSort of (1GateCircStr p,f,x) = {[p,f]} by FUNCT_2:def 1;
A14: the ResultSort of (1GateCircStr p,f,x) . [p,f] = x by Def5;
A15: the Arity of (1GateCircStr p,f,x) . [p,f] = p by Def5;
A16: len p = n by FINSEQ_1:def 18;
A17: dom the Arity of (1GateCircStr p,f,x) = {[p,f]} by A12, FUNCT_2:def 1;

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) )
A18: (SORTS # ) . pp = n -tuples_on X by A16, A11, Th6;
assume A19: 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 A20: i = [p,f] by A12, TARSKI:def 1;
then A21: ((SORTS # ) * the Arity of (1GateCircStr p,f,x)) . i = (SORTS # ) . p by A12, A15, A17, A19, FUNCT_1:23;
(SORTS * the ResultSort of (1GateCircStr p,f,x)) . i = Y by A12, A14, A4, A13, A19, A20, 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) by A19, A21, A18, FUNCOP_1:13; :: 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 A12, FUNCOP_1:13; :: thesis: verum