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 FINSEQ_1:def 18;
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:13;
A9:
dom the Arity of (1GateCircStr p,f) = {[p,f]}
by A4, FUNCT_2:def 1;
now let i be
set ;
( 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, Th6;
assume A11:
i in the
carrier' of
(1GateCircStr p,f)
;
(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:23;
((the carrier of (1GateCircStr p,f) --> X) * the ResultSort of (1GateCircStr p,f)) . i = X
by A4, A3, A8, A5, A11, A12, FUNCT_1:23;
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:13;
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 18;
reconsider A = MSAlgebra(# (the carrier of (1GateCircStr p,f) --> X),CHARACT #) as strict non-empty MSAlgebra of 1GateCircStr p,f by MSUALG_1:def 8;
take
A
; ( 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:13; verum