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
for f being Function st the_arity_of o = {} & dom f = I & ( for i being Element of I holds f . i = const o,(A . i) ) holds
f = const o,(product A)
let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for f being Function st the_arity_of o = {} & dom f = I & ( for i being Element of I holds f . i = const o,(A . i) ) holds
f = const o,(product A)
let A be MSAlgebra-Family of I,S; :: thesis: for o being OperSymbol of S
for f being Function st the_arity_of o = {} & dom f = I & ( for i being Element of I holds f . i = const o,(A . i) ) holds
f = const o,(product A)
let o be OperSymbol of S; :: thesis: for f being Function st the_arity_of o = {} & dom f = I & ( for i being Element of I holds f . i = const o,(A . i) ) holds
f = const o,(product A)
let f be Function; :: thesis: ( the_arity_of o = {} & dom f = I & ( for i being Element of I holds f . i = const o,(A . i) ) implies f = const o,(product A) )
assume that
A1: the_arity_of o = {} and
A2: dom f = I and
A3: for i being Element of I holds f . i = const o,(A . i) ; :: thesis: f = const o,(product A)

A4: now

let a be set ; :: thesis: ( a in I implies f . a = (const o,(product A)) . a )
assume a in I ; :: thesis: f . a = (const o,(product A)) . a
then reconsider a9 = a as Element of I ;
thus f . a = const o,(A . a9) by A3
.= (const o,(product A)) . a by A1, Th10 ; :: thesis: verum

end;

set C = union { (Result o,(A . i9)) where i9 is Element of I : verum } ;
const o,(product A) in Funcs I,(union { (Result o,(A . i9)) where i9 is Element of I : verum } ) by A1, Th9;
then ex g2 being Function st
( g2 = const o,(product A) & dom g2 = I & rng g2 c= union { (Result o,(A . i9)) where i9 is Element of I : verum } ) by FUNCT_2:def 2;
hence f = const o,(product A) by A2, A4, FUNCT_1:9; :: thesis: verum