let I be non empty set ; :: thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S st the_arity_of o = {} holds
const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))
let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S st the_arity_of o = {} holds
const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))
let A be MSAlgebra-Family of I,S; :: thesis: for o being OperSymbol of S st the_arity_of o = {} holds
const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))
let o be OperSymbol of S; :: thesis: ( the_arity_of o = {} implies const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) )
set g = (commute (OPER A)) . o;
set C = union { (Result (o,(A . i9))) where i9 is Element of I : verum } ;
assume A1: the_arity_of o = {} ; :: thesis: const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))
then A2: (commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )))) by Th7;
reconsider g = (commute (OPER A)) . o as Function ;
(OPS A) . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) by PRALG_2:def 13
.= commute (A ?. o) by A1, FUNCOP_1:def 8 ;
then A3: const (o,(product A)) = (commute g) . {} by MSUALG_1:def 6;
commute g in Funcs ({{}},(Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )))) by A2, FUNCT_6:55;
then consider g1 being Function such that
A4: g1 = commute g and
A5: dom g1 = {{}} and
A6: rng g1 c= Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) by FUNCT_2:def 2;
{} in {{}} by TARSKI:def 1;
then g1 . {} in rng g1 by A5, FUNCT_1:def 3;
hence const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) by A3, A4, A6; :: thesis: verum