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 . i')) where i' 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 . i')) where i' 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 . i')) where i' 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 . i')) where i' is Element of I : verum } )) )
assume A1: the_arity_of o = {} ; :: thesis: (commute (OPER A)) . o in Funcs I,(Funcs {{} },(union { (Result o,(A . i')) where i' is Element of I : verum } ))
set f = (commute (OPER A)) . o;
commute (OPER A) in Funcs the carrier' of S,(Funcs I,(rng (uncurry (OPER A)))) by PRALG_2:13;
then consider f1 being Function such that
A2: commute (OPER A) = f1 and
A3: dom f1 = the carrier' of S and
A4: rng f1 c= Funcs I,(rng (uncurry (OPER A))) by FUNCT_2:def 2;
(commute (OPER A)) . o in rng (commute (OPER A)) by A2, A3, FUNCT_1:def 5;
then consider fb being Function such that
A5: ( fb = (commute (OPER A)) . o & dom fb = I & rng fb c= rng (uncurry (OPER A)) ) by A2, A4, FUNCT_2:def 2;
set C = union { (Result o,(A . i')) where i' is Element of I : verum } ;

now

let x be set ; :: thesis: ( x in rng ((commute (OPER A)) . o) implies x in Funcs {{} },(union { (Result o,(A . i')) where i' is Element of I : verum } ) )
assume A6: x in rng ((commute (OPER A)) . o) ; :: thesis: x in Funcs {{} },(union { (Result o,(A . i')) where i' is Element of I : verum } )
A7: (commute (OPER A)) . o = A ?. o ;
consider a being set such that
A8: ( a in dom ((commute (OPER A)) . o) & ((commute (OPER A)) . o) . a = x ) by A6, FUNCT_1:def 5;
reconsider a = a as Element of I by A5, A8;
reconsider x' = x as Function by A7, A8;
A9: x' = (A ?. o) . a by A8
.= Den o,(A . a) by PRALG_2:14 ;
then A10: dom x' = Args o,(A . a) by FUNCT_2:def 1
.= {{} } by A1, PRALG_2:11 ;

now

let c be set ; :: thesis: ( c in rng x' implies c in union { (Result o,(A . i')) where i' is Element of I : verum } )
assume c in rng x' ; :: thesis: c in union { (Result o,(A . i')) where i' is Element of I : verum }
then consider b being set such that
A11: ( b in dom x' & x' . b = c ) by FUNCT_1:def 5;
x' . b = const o,(A . a) by A9, A10, A11, TARSKI:def 1;
then A12: c is Element of Result o,(A . a) by A1, A11, Th6;
Result o,(A . a) in { (Result o,(A . i')) where i' is Element of I : verum } ;
hence c in union { (Result o,(A . i')) where i' is Element of I : verum } by A12, TARSKI:def 4; :: thesis: verum

end;

then rng x' c= union { (Result o,(A . i')) where i' is Element of I : verum } by TARSKI:def 3;
hence x in Funcs {{} },(union { (Result o,(A . i')) where i' is Element of I : verum } ) by A10, FUNCT_2:def 2; :: thesis: verum

end;

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