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)
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)
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 f = (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;
A4: const o,(product A) = (commute ((commute (OPER A)) . o)) . {} by A2, MSUALG_1:def 11;
consider f' being Function;
consider g being Function;
A5: {} in {{} } by TARSKI:def 1;
const o,(A . i) = ((A ?. o) . i) . {} by PRALG_2:14
.= (const o,(product A)) . i by A3, A4, A5, FUNCT_6:86 ;
hence (const o,(product A)) . i = const o,(A . i) ; :: thesis: verum