set f = uncurry (OPER A);
set C = commute (OPER A);
A1: dom (uncurry (OPER A)) = [:I, the carrier' of S:] by Th5;

per cases ( I <> {} or I = {} ) ;

suppose A2: I <> {} ; :: thesis: (commute (OPER A)) . o is ManySortedFunction of I

then commute (OPER A) in Funcs ( the carrier' of S,(Funcs (I,(rng (uncurry (OPER A)))))) by Th6;
then A3: ex a being Function st
( a = commute (OPER A) & dom a = the carrier' of S & rng a 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 consider g being Function such that
A4: g = (commute (OPER A)) . o and
A5: dom g = I and
rng g c= rng (uncurry (OPER A)) by A3, FUNCT_2:def 2;
reconsider g = g as ManySortedSet of I by A5, PARTFUN1:def 2, RELAT_1:def 18;
for x being object st x in dom g holds
g . x is Function

proof

let x be object ; :: thesis: ( x in dom g implies g . x is Function )
assume x in dom g ; :: thesis: g . x is Function
then reconsider i = x as Element of I by A5;
A6: ( [i,o] `1 = i & [i,o] `2 = o ) ;
consider U0 being MSAlgebra over S such that
U0 = A . i and
A7: (OPER A) . i = the Charact of U0 by A2, Def11;
A8: [i,o] in dom (uncurry (OPER A)) by A1, A2, ZFMISC_1:87;
then g . i = (uncurry (OPER A)) . (i,o) by A4, FUNCT_5:22;
then g . i = the Charact of U0 . o by A8, A6, A7, FUNCT_5:def 2
.= Den (o,U0) by MSUALG_1:def 6 ;
hence g . x is Function ; :: thesis: verum

end;

hence (commute (OPER A)) . o is ManySortedFunction of I by A4, FUNCOP_1:def 6; :: thesis: verum

end;

suppose A9: I = {} ; :: thesis: (commute (OPER A)) . o is ManySortedFunction of I

reconsider f = EmptyMS I as ManySortedFunction of I ;
f = {} by A9
.= (commute {}) . o by FUNCT_6:58
.= (commute (OPER A)) . o by A9 ;
hence (commute (OPER A)) . o is ManySortedFunction of I ; :: thesis: verum

end;

end;