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;
A1: dom (x .--> Y) = {x} by FUNCOP_1:13;
A2: x in {x} by TARSKI:def 1;
then A3: (((rng p) --> X) +* (x .--> Y)) . x = (x .--> Y) . x by A1, FUNCT_4:13
.= Y by A2, FUNCOP_1:7 ;
A4: 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 A4, 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;
A5: dom (((rng p) --> X) #) = (rng p) * by PARTFUN1:def 2;
A6: dom ((rng p) --> X) = rng p by FUNCOP_1:13;
(rng p) --> X tolerates x .--> Y

proof

let y be set ; :: according to PARTFUN1:def 4 :: thesis: ( not y in (proj1 ((rng p) --> X)) /\ (proj1 (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 rng p by A6, XBOOLE_0:def 4;
then A8: ((rng p) --> X) . y = X by FUNCOP_1:7;
A9: y in {x} by A1, A7, XBOOLE_0:def 4;
then x = y by TARSKI:def 1;
hence ((rng p) --> X) . y = (x .--> Y) . y by B1, A6, A7, A9, A8, FUNCOP_1:7, XBOOLE_0:def 4; :: thesis: verum

end;

then (rng p) --> X c= SORTS by FUNCT_4:28;
then ((rng p) --> X) # c= SORTS # by Th1;
then A10: (((rng p) --> X) #) . p9 = (SORTS #) . pp by A5, GRFUNC_1:2;
A11: the carrier' of (1GateCircStr (p,f,x)) = {[p,f]} by Def5;
then A12: dom the ResultSort of (1GateCircStr (p,f,x)) = {[p,f]} by FUNCT_2:def 1;
A13: the ResultSort of (1GateCircStr (p,f,x)) . [p,f] = x by Def5;
A14: the Arity of (1GateCircStr (p,f,x)) . [p,f] = p by Def5;
A15: len p = n by CARD_1:def 7;
A16: dom the Arity of (1GateCircStr (p,f,x)) = {[p,f]} by A11, FUNCT_2:def 1;

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

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) )
A17: (SORTS #) . pp = n -tuples_on X by A15, A10, Th2;
assume A18: 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 A19: i = [p,f] by A11, TARSKI:def 1;
then A20: ((SORTS #) * the Arity of (1GateCircStr (p,f,x))) . i = (SORTS #) . p by A11, A14, A16, A18, FUNCT_1:13;
(SORTS * the ResultSort of (1GateCircStr (p,f,x))) . i = Y by A11, A13, A3, A12, A18, A19, FUNCT_1:13;
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 A18, A20, A17, FUNCOP_1:7; :: 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 15;
reconsider A = MSAlgebra(# SORTS,CHARACT #) as strict non-empty MSAlgebra over 1GateCircStr (p,f,x) by MSUALG_1:def 3;
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 A11, FUNCOP_1:7; :: thesis: verum