let I be non empty set ; :: thesis: for S being non empty non void ManySortedSign
for i being Element of I
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S st the_arity_of o = {} holds
(const o,(product A)) . i = const o,(A . i)
let S be non empty non void ManySortedSign ; :: thesis: for i being Element of I
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S st the_arity_of o = {} holds
(const o,(product A)) . i = const o,(A . i)
let i be Element of I; :: 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)) . i = const o,(A . i)
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)) . i = const o,(A . i)
consider g being Function;
consider f9 being Function;
let o be OperSymbol of S; :: thesis: ( the_arity_of o = {} implies (const o,(product A)) . i = const o,(A . i) )
assume A1: the_arity_of o = {} ; :: thesis: (const o,(product A)) . i = const o,(A . i)
set f = (commute (OPER A)) . o;
set C = union { (Result o,(A . i9)) where i9 is Element of I : verum } ;
A2: (commute (OPER A)) . o in Funcs I,(Funcs {{} },(union { (Result o,(A . i9)) where i9 is Element of I : verum } )) by A1, Th8;
(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 ;
then A3: const o,(product A) = (commute ((commute (OPER A)) . o)) . {} by MSUALG_1:def 11;
A4: {} in {{} } by TARSKI:def 1;
const o,(A . i) = ((A ?. o) . i) . {} by PRALG_2:14
.= (const o,(product A)) . i by A2, A3, A4, FUNCT_6:86 ;
hence (const o,(product A)) . i = const o,(A . i) ; :: thesis: verum