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 = {} & dom f = I ) and
A2: for i being Element of I holds f . i = const o,(A . i) ; :: thesis: f = const o,(product A)
set C = union { (Result o,(A . i')) where i' is Element of I : verum } ;
const o,(product A) in Funcs I,(union { (Result o,(A . i')) where i' is Element of I : verum } ) by A1, Th9;
then consider g2 being Function such that
A3: ( g2 = const o,(product A) & dom g2 = I & rng g2 c= union { (Result o,(A . i')) where i' is Element of I : verum } ) by FUNCT_2:def 2;

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 a' = a as Element of I ;
thus f . a = const o,(A . a') by A2
.= (const o,(product A)) . a by A1, Th10 ; :: thesis: verum

end;

hence f = const o,(product A) by A1, A3, FUNCT_1:9; :: thesis: verum