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 2;
CHARACT is Function-yielding
proof
let x be object ; :: 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 2;
reconsider p = the Arity of F1() . o as Element of the carrier of F1() * by A3, A4, FUNCT_2:5;
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 :: thesis: for i being object st i in the carrier' of F1() holds
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)
let i be object ; :: 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:5;
A8: ((( the carrier of F1() --> BOOLEAN) #) * the Arity of F1()) . i = (( the carrier of F1() --> BOOLEAN) #) . p by A6, A7, FUNCT_1:13;
reconsider v = the ResultSort of F1() . o as Vertex of F1() by A7, FUNCT_2:5;
( the carrier of F1() --> BOOLEAN) . v = BOOLEAN ;
then A9: (( the carrier of F1() --> BOOLEAN) * the ResultSort of F1()) . i = BOOLEAN by A5, A7, FUNCT_1:13;
A10: (( the carrier of F1() --> BOOLEAN) #) . p = (len p) -tuples_on BOOLEAN by Th2;
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 15;
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