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))
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, Th7;
(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 ((commute (OPER A)) . o)) . {} by MSUALG_1:def 6;
A4: {} in {{}} by TARSKI:def 1;
const (o,(A . i)) = ((A ?. o) . i) . {} by PRALG_2:7
.= (const (o,(product A))) . i by A2, A3, A4, FUNCT_6:56 ;
hence (const (o,(product A))) . i = const (o,(A . i)) ; :: thesis: verum