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 st the_arity_of o = {} holds
(commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))))
let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S st the_arity_of o = {} holds
(commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))))
let A be MSAlgebra-Family of I,S; :: thesis: for o being OperSymbol of S st the_arity_of o = {} holds
(commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))))
let o be OperSymbol of S; :: thesis: ( the_arity_of o = {} implies (commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )))) )
set f = (commute (OPER A)) . o;
set C = union { (Result (o,(A . i9))) where i9 is Element of I : verum } ;
commute (OPER A) in Funcs ( the carrier' of S,(Funcs (I,(rng (uncurry (OPER A)))))) by PRALG_2:6;
then A1: ex f1 being Function st
( commute (OPER A) = f1 & dom f1 = the carrier' of S & rng f1 c= Funcs (I,(rng (uncurry (OPER A)))) ) by FUNCT_2:def 2;
then (commute (OPER A)) . o in rng (commute (OPER A)) by FUNCT_1:def 3;
then A2: ex fb being Function st
( fb = (commute (OPER A)) . o & dom fb = I & rng fb c= rng (uncurry (OPER A)) ) by A1, FUNCT_2:def 2;
assume A3: the_arity_of o = {} ; :: thesis: (commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))))

now :: thesis: for x being object st x in rng ((commute (OPER A)) . o) holds
x in Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))

let x be object ; :: thesis: ( x in rng ((commute (OPER A)) . o) implies x in Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) )
assume x in rng ((commute (OPER A)) . o) ; :: thesis: x in Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))
then consider a being object such that
A4: a in dom ((commute (OPER A)) . o) and
A5: ((commute (OPER A)) . o) . a = x by FUNCT_1:def 3;
(commute (OPER A)) . o = A ?. o ;
then reconsider x9 = x as Function by A5;
reconsider a = a as Element of I by A2, A4;
A6: x9 = (A ?. o) . a by A5
.= Den (o,(A . a)) by PRALG_2:7 ;
then A7: dom x9 = Args (o,(A . a)) by FUNCT_2:def 1
.= {{}} by A3, PRALG_2:4 ;

now :: thesis: for c being object st c in rng x9 holds
c in union { (Result (o,(A . i9))) where i9 is Element of I : verum }

let c be object ; :: thesis: ( c in rng x9 implies c in union { (Result (o,(A . i9))) where i9 is Element of I : verum } )
assume c in rng x9 ; :: thesis: c in union { (Result (o,(A . i9))) where i9 is Element of I : verum }
then consider b being object such that
A8: b in dom x9 and
A9: x9 . b = c by FUNCT_1:def 3;
x9 . b = const (o,(A . a)) by A6, A7, A8, TARSKI:def 1;
then A10: c is Element of Result (o,(A . a)) by A3, A9, Th5;
Result (o,(A . a)) in { (Result (o,(A . i9))) where i9 is Element of I : verum } ;
hence c in union { (Result (o,(A . i9))) where i9 is Element of I : verum } by A10, TARSKI:def 4; :: thesis: verum

end;

then rng x9 c= union { (Result (o,(A . i9))) where i9 is Element of I : verum } ;
hence x in Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) by A7, FUNCT_2:def 2; :: thesis: verum

end;

then rng ((commute (OPER A)) . o) c= Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) ;
hence (commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )))) by A2, FUNCT_2:def 2; :: thesis: verum