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 :: thesis: for a being object st a in I holds
f . a = (const (o,(product A))) . a

let a be object ; :: 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, Th9 ; :: 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, Th8;
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; :: thesis: verum