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 <> {}
;
(commute (OPER A)) . o is ManySortedFunction of Ithen
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 ;
( x in dom g implies g . x is Function )
assume
x in dom g
;
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
;
verum
end; hence
(commute (OPER A)) . o is
ManySortedFunction of
I
by A4, FUNCOP_1:def 6;
verum end;