set S = F1();
set SORTS = the carrier of F1() --> BOOLEAN ;
consider CHARACT being ManySortedSet of the carrier' of F1() such that
A2: for o being set
for p being Element of the carrier of F1() * st o in the carrier' of F1() & p = the Arity of F1() . o holds
CHARACT . o = F2(o,p) from CIRCCOMB:sch 1();
 A3: dom CHARACT = the carrier' of F1() by PARTFUN1:def 4;
CHARACT is Function-yielding
proof
let x be set ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 CHARACT or CHARACT . x is set )
assume A4: x in dom CHARACT ; :: thesis: CHARACT . x is set
then reconsider o = x as Gate of F1() by PARTFUN1:def 4;
reconsider p = the Arity of F1() . o as Element of the carrier of F1() * by A3, A4, FUNCT_2:7;
CHARACT . x = F2(o,p) by A2, A3, A4;
hence CHARACT . x is set by A1, A3, A4; :: thesis: verum
end;
then reconsider CHARACT = CHARACT as ManySortedFunction of the carrier' of F1() ;
A5: dom the ResultSort of F1() = the carrier' of F1() by FUNCT_2:def 1;
A6: dom the Arity of F1() = the carrier' of F1() by FUNCT_2:def 1;
now
let i be set ; :: thesis: ( i in the carrier' of F1() implies CHARACT . i is Function of ((((the carrier of F1() --> BOOLEAN ) # ) * the Arity of F1()) . i),(((the carrier of F1() --> BOOLEAN ) * the ResultSort of F1()) . i) )
assume A7: i in the carrier' of F1() ; :: thesis: CHARACT . i is Function of ((((the carrier of F1() --> BOOLEAN ) # ) * the Arity of F1()) . i),(((the carrier of F1() --> BOOLEAN ) * the ResultSort of F1()) . i)
then reconsider o = i as Gate of F1() ;
reconsider p = the Arity of F1() . o as Element of the carrier of F1() * by A7, FUNCT_2:7;
A8: (((the carrier of F1() --> BOOLEAN ) # ) * the Arity of F1()) . i = ((the carrier of F1() --> BOOLEAN ) # ) . p by A6, A7, FUNCT_1:23;
reconsider v = the ResultSort of F1() . o as Vertex of F1() by A7, FUNCT_2:7;
(the carrier of F1() --> BOOLEAN ) . v = BOOLEAN by FUNCOP_1:13;
then A9: ((the carrier of F1() --> BOOLEAN ) * the ResultSort of F1()) . i = BOOLEAN by A5, A7, FUNCT_1:23;
A10: ((the carrier of F1() --> BOOLEAN ) # ) . p = (len p) -tuples_on BOOLEAN by Th6;
CHARACT . i = F2(o,p) by A2, A7;
hence CHARACT . i is Function of ((((the carrier of F1() --> BOOLEAN ) # ) * the Arity of F1()) . i),(((the carrier of F1() --> BOOLEAN ) * the ResultSort of F1()) . i) by A1, A7, A8, A10, A9; :: thesis: verum
end;
then reconsider CHARACT = CHARACT as ManySortedFunction of ((the carrier of F1() --> BOOLEAN ) # ) * the Arity of F1(),(the carrier of F1() --> BOOLEAN ) * the ResultSort of F1() by PBOOLE:def 18;
take MSAlgebra(# (the carrier of F1() --> BOOLEAN ),CHARACT #) ; :: thesis: ( the Sorts of MSAlgebra(# (the carrier of F1() --> BOOLEAN ),CHARACT #) = the carrier of F1() --> BOOLEAN & ( for g being set
for p being Element of the carrier of F1() * st g in the carrier' of F1() & p = the Arity of F1() . g holds
the Charact of MSAlgebra(# (the carrier of F1() --> BOOLEAN ),CHARACT #) . g = F2(g,p) ) )
thus ( the Sorts of MSAlgebra(# (the carrier of F1() --> BOOLEAN ),CHARACT #) = the carrier of F1() --> BOOLEAN & ( for g being set
for p being Element of the carrier of F1() * st g in the carrier' of F1() & p = the Arity of F1() . g holds
the Charact of MSAlgebra(# (the carrier of F1() --> BOOLEAN ),CHARACT #) . g = F2(g,p) ) ) by A2; :: thesis: verum