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
for x being Element of Args (o,(product A)) st the_arity_of o <> {} holds
for i being Element of I holds (proj (A,i)) # x = (commute x) . i
let S be non empty non void ManySortedSign ; for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being Element of Args (o,(product A)) st the_arity_of o <> {} holds
for i being Element of I holds (proj (A,i)) # x = (commute x) . i
let A be MSAlgebra-Family of I,S; for o being OperSymbol of S
for x being Element of Args (o,(product A)) st the_arity_of o <> {} holds
for i being Element of I holds (proj (A,i)) # x = (commute x) . i
let o be OperSymbol of S; for x being Element of Args (o,(product A)) st the_arity_of o <> {} holds
for i being Element of I holds (proj (A,i)) # x = (commute x) . i
let x be Element of Args (o,(product A)); ( the_arity_of o <> {} implies for i being Element of I holds (proj (A,i)) # x = (commute x) . i )
assume A1:
the_arity_of o <> {}
; for i being Element of I holds (proj (A,i)) # x = (commute x) . i
set C = union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ;
let i be Element of I; (proj (A,i)) # x = (commute x) . i
A2:
x 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 A3:
commute x 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
dom (commute x) = I
by FUNCT_2:92;
then A4:
(commute x) . i in rng (commute x)
by FUNCT_1:def 3;
SS:
dom x = dom (the_arity_of o)
by MSUALG_6:2;
A5:
now for n being object st n in dom (the_arity_of o) holds
((proj (A,i)) # x) . n = ((commute x) . i) . nA6:
rng x c= 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 A2, FUNCT_2:92;
let n be
object ;
( n in dom (the_arity_of o) implies ((proj (A,i)) # x) . n = ((commute x) . i) . n )assume A7:
n in dom (the_arity_of o)
;
((proj (A,i)) # x) . n = ((commute x) . i) . n
x . n in product (Carrier (A,((the_arity_of o) /. n)))
by A7, Th15;
then A8:
x . n in dom (proj ((Carrier (A,((the_arity_of o) /. n))),i))
by CARD_3:def 16;
n in dom x
by A2, A7, FUNCT_2:92;
then
x . n in rng x
by FUNCT_1:def 3;
then consider g being
Function such that A9:
g = x . n
and
dom g = I
and
rng g c= union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum }
by A6, FUNCT_2:def 2;
thus ((proj (A,i)) # x) . n =
((proj (A,i)) . ((the_arity_of o) /. n)) . (x . n)
by A7, Th13
.=
(proj ((Carrier (A,((the_arity_of o) /. n))),i)) . (x . n)
by Def2
.=
g . i
by A9, A8, CARD_3:def 16
.=
((commute x) . i) . n
by A2, A7, A9, FUNCT_6:56
;
verum end;
A10:
x in product (doms ((proj (A,i)) * (the_arity_of o)))
by Th12;
rng (commute x) c= 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 A3, FUNCT_2:92;
then A11:
dom ((commute x) . i) = dom (the_arity_of o)
by A4, FUNCT_2:92;
dom (proj (A,i)) = the carrier of S
by PARTFUN1:def 2;
then A12:
rng (the_arity_of o) c= dom (proj (A,i))
;
dom ((proj (A,i)) # x) =
dom ((Frege ((proj (A,i)) * (the_arity_of o))) . x)
by MSUALG_3:def 5
.=
dom (((proj (A,i)) * (the_arity_of o)) .. x)
by A10, PRALG_2:def 2
.=
(dom ((proj (A,i)) * (the_arity_of o))) /\ (dom x)
by PRALG_1:def 19
.=
(dom (the_arity_of o)) /\ (dom x)
by A12, RELAT_1:27
;
hence
(proj (A,i)) # x = (commute x) . i
by A11, A5, SS; verum