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} ;
A3: x in {x} by TARSKI:def 1;
then A4: (((rng p) --> X) +* (x .--> Y)) . x = (x .--> Y) . x by A2, FUNCT_4:13
.= Y by A3, FUNCOP_1:7 ;
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 2;
(rng p) --> X tolerates x .--> Y
proof
let y be object ; :: 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 A8: y in (dom ((rng p) --> X)) /\ (dom (x .--> Y)) ; :: thesis: ((rng p) --> X) . y = (x .--> Y) . y
then y in rng p by XBOOLE_0:def 4;
then A9: ((rng p) --> X) . y = X by FUNCOP_1:7;
A10: y in {x} by A8, XBOOLE_0:def 4;
then x = y by TARSKI:def 1;
hence ((rng p) --> X) . y = (x .--> Y) . y by A1, A8, A10, A9, 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 A11: (((rng p) --> X) #) . p9 = (SORTS #) . pp by A6, GRFUNC_1:2;
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 CARD_1:def 7;
A17: dom the Arity of (1GateCircStr (p,f,x)) = {[p,f]} by A12, FUNCT_2:def 1;
now :: thesis: for i being object 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 object ; :: 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, Th2;
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:13;
(SORTS * the ResultSort of (1GateCircStr (p,f,x))) . i = Y by A12, A14, A4, A13, A19, A20, 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 A19, A21, A18, 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 A12, FUNCOP_1:7; :: thesis: verum