let I be non empty set ; 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
for y being Element of Args (o,(product A))
for i9 being Element of I
for g being Function st g = (Den (o,(product A))) . y holds
g . i9 = (Den (o,(A . i9))) . ((commute y) . i9)
let S be 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
for y being Element of Args (o,(product A))
for i9 being Element of I
for g being Function st g = (Den (o,(product A))) . y holds
g . i9 = (Den (o,(A . i9))) . ((commute y) . i9)
let A be MSAlgebra-Family of I,S; for o being OperSymbol of S st the_arity_of o <> {} holds
for y being Element of Args (o,(product A))
for i9 being Element of I
for g being Function st g = (Den (o,(product A))) . y holds
g . i9 = (Den (o,(A . i9))) . ((commute y) . i9)
let o be OperSymbol of S; ( the_arity_of o <> {} implies for y being Element of Args (o,(product A))
for i9 being Element of I
for g being Function st g = (Den (o,(product A))) . y holds
g . i9 = (Den (o,(A . i9))) . ((commute y) . i9) )
assume A1:
the_arity_of o <> {}
; for y being Element of Args (o,(product A))
for i9 being Element of I
for g being Function st g = (Den (o,(product A))) . y holds
g . i9 = (Den (o,(A . i9))) . ((commute y) . i9)
let y be Element of Args (o,(product A)); for i9 being Element of I
for g being Function st g = (Den (o,(product A))) . y holds
g . i9 = (Den (o,(A . i9))) . ((commute y) . i9)
let i9 be Element of I; for g being Function st g = (Den (o,(product A))) . y holds
g . i9 = (Den (o,(A . i9))) . ((commute y) . i9)
A2:
y in dom (Commute (Frege (A ?. o)))
by A1, Th18;
A3:
commute y in product (doms (A ?. o))
by A1, Th17;
A4: Den (o,(product A)) =
(OPS A) . o
by MSUALG_1:def 6
.=
IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o))))
by PRALG_2:def 13
.=
Commute (Frege (A ?. o))
by A1, FUNCOP_1:def 8
;
set C = union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ;
y in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ))))
by Th14;
then
commute y in Funcs (I,(Funcs ((dom (the_arity_of o)),(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ))))
by A1, FUNCT_6:55;
then WW:
dom (commute y) = I
by FUNCT_2:92;
dom (A ?. o) = I
by PARTFUN1:def 2;
then a5: dom ((A ?. o) .. (commute y)) =
I /\ (dom (commute y))
by PRALG_1:def 19
.=
I
by WW
;
let g be Function; ( g = (Den (o,(product A))) . y implies g . i9 = (Den (o,(A . i9))) . ((commute y) . i9) )
assume
g = (Den (o,(product A))) . y
; g . i9 = (Den (o,(A . i9))) . ((commute y) . i9)
then g =
(Frege (A ?. o)) . (commute y)
by A4, A2, PRALG_2:def 1
.=
(A ?. o) .. (commute y)
by A3, PRALG_2:def 2
;
then g . i9 =
((A ?. o) . i9) . ((commute y) . i9)
by a5, PRALG_1:def 19
.=
(Den (o,(A . i9))) . ((commute y) . i9)
by PRALG_2:7
;
hence
g . i9 = (Den (o,(A . i9))) . ((commute y) . i9)
; verum