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
for y being Element of Args o,(product A) st the_arity_of o <> {} holds
commute y in product (doms (A ?. o))
let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for y being Element of Args o,(product A) st the_arity_of o <> {} holds
commute y in product (doms (A ?. o))
let A be MSAlgebra-Family of I,S; :: thesis: for o being OperSymbol of S
for y being Element of Args o,(product A) st the_arity_of o <> {} holds
commute y in product (doms (A ?. o))
let o be OperSymbol of S; :: thesis: for y being Element of Args o,(product A) st the_arity_of o <> {} holds
commute y in product (doms (A ?. o))
let y be Element of Args o,(product A); :: thesis: ( the_arity_of o <> {} implies commute y in product (doms (A ?. o)) )
assume
the_arity_of o <> {}
; :: thesis: commute y in product (doms (A ?. o))
then A1:
dom (the_arity_of o) <> {}
;
set D = union { (the Sorts of (A . i') . s') where i' is Element of I, s' is Element of the carrier of S : verum } ;
A2:
y in Funcs (dom (the_arity_of o)),(Funcs I,(union { (the Sorts of (A . i') . s') where i' is Element of I, s' is Element of the carrier of S : verum } ))
by Th15;
then
commute y in Funcs I,(Funcs (dom (the_arity_of o)),(union { (the Sorts of (A . i') . s') where i' is Element of I, s' is Element of the carrier of S : verum } ))
by A1, FUNCT_6:85;
then consider f being Function such that
A3:
( f = commute y & dom f = I & rng f c= Funcs (dom (the_arity_of o)),(union { (the Sorts of (A . i') . s') where i' is Element of I, s' is Element of the carrier of S : verum } ) )
by FUNCT_2:def 2;
A4:
dom (commute y) = dom (doms (A ?. o))
by A3, PRALG_2:18;
now let i1 be
set ;
:: thesis: ( i1 in dom (doms (A ?. o)) implies (commute y) . i1 in (doms (A ?. o)) . i1 )assume
i1 in dom (doms (A ?. o))
;
:: thesis: (commute y) . i1 in (doms (A ?. o)) . i1then reconsider ii =
i1 as
Element of
I by PRALG_2:18;
(commute y) . ii in rng (commute y)
by A3, FUNCT_1:def 5;
then consider h being
Function such that A5:
(
h = (commute y) . ii &
dom h = dom (the_arity_of o) &
rng h c= union { (the Sorts of (A . i') . s') where i' is Element of I, s' is Element of the carrier of S : verum } )
by A3, FUNCT_2:def 2;
A6:
dom ((commute y) . ii) = dom (the Sorts of (A . ii) * (the_arity_of o))
by A5, PRALG_2:10;
now let n be
set ;
:: thesis: ( n in dom (the Sorts of (A . ii) * (the_arity_of o)) implies ((commute y) . ii) . n in (the Sorts of (A . ii) * (the_arity_of o)) . n )assume A7:
n in dom (the Sorts of (A . ii) * (the_arity_of o))
;
:: thesis: ((commute y) . ii) . n in (the Sorts of (A . ii) * (the_arity_of o)) . nthen A8:
n in dom (the_arity_of o)
by PRALG_2:10;
then
(the_arity_of o) . n in rng (the_arity_of o)
by FUNCT_1:def 5;
then reconsider s1 =
(the_arity_of o) . n as
SortSymbol of
S ;
consider ff being
Function such that A9:
(
ff = y &
dom ff = dom (the_arity_of o) &
rng ff c= Funcs I,
(union { (the Sorts of (A . i') . s') where i' is Element of I, s' is Element of the carrier of S : verum } ) )
by A2, FUNCT_2:def 2;
n in dom y
by A7, A9, PRALG_2:10;
then
y . n in rng y
by FUNCT_1:def 5;
then consider g being
Function such that A10:
(
g = y . n &
dom g = I &
rng g c= union { (the Sorts of (A . i') . s') where i' is Element of I, s' is Element of the carrier of S : verum } )
by A9, FUNCT_2:def 2;
A11:
((commute y) . ii) . n = g . ii
by A2, A8, A10, FUNCT_6:86;
g . ii in the
Sorts of
(A . ii) . s1
by A8, A10, Th17;
hence
((commute y) . ii) . n in (the Sorts of (A . ii) * (the_arity_of o)) . n
by A7, A11, FUNCT_1:22;
:: thesis: verum end; then
(commute y) . ii in product (the Sorts of (A . ii) * (the_arity_of o))
by A6, CARD_3:18;
then
(commute y) . ii in Args o,
(A . ii)
by PRALG_2:10;
hence
(commute y) . i1 in (doms (A ?. o)) . i1
by PRALG_2:18;
:: thesis: verum end;
hence
commute y in product (doms (A ?. o))
by A4, CARD_3:18; :: thesis: verum