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 . i')) where i' 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 . i')) where i' 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 . i')) where i' 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 . i')) where i' is Element of I : verum } ) )
assume A1: the_arity_of o = {} ; :: thesis: const o,(product A) in Funcs I,(union { (Result o,(A . i')) where i' is Element of I : verum } )
A2: (OPS A) . o = IFEQ (the_arity_of o),{} ,(commute (A ?. o)),(Commute (Frege (A ?. o))) by PRALG_2:def 20
.= commute (A ?. o) by A1, FUNCOP_1:def 8 ;
set g = (commute (OPER A)) . o;
set C = union { (Result o,(A . i')) where i' is Element of I : verum } ;
A3: (commute (OPER A)) . o in Funcs I,(Funcs {{} },(union { (Result o,(A . i')) where i' is Element of I : verum } )) by A1, Th8;
reconsider g = (commute (OPER A)) . o as Function ;
A4: const o,(product A) = (commute g) . {} by A2, MSUALG_1:def 11;
A5: {} in {{} } by TARSKI:def 1;
commute g in Funcs {{} },(Funcs I,(union { (Result o,(A . i')) where i' is Element of I : verum } )) by A3, FUNCT_6:85;
then consider g1 being Function such that
A6: ( g1 = commute g & dom g1 = {{} } & rng g1 c= Funcs I,(union { (Result o,(A . i')) where i' is Element of I : verum } ) ) by FUNCT_2:def 2;
g1 . {} in rng g1 by A5, A6, FUNCT_1:def 5;
hence const o,(product A) in Funcs I,(union { (Result o,(A . i')) where i' is Element of I : verum } ) by A4, A6; :: thesis: verum