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 st the_arity_of o <> {} holds
for y being Element of Args o,(product A)
for i' being Element of I
for g being Function st g = (Den o,(product A)) . y holds
g . i' = (Den o,(A . i')) . ((commute y) . i')
let S be non empty non void ManySortedSign ; :: thesis: 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 i' being Element of I
for g being Function st g = (Den o,(product A)) . y holds
g . i' = (Den o,(A . i')) . ((commute y) . i')
let A be MSAlgebra-Family of I,S; :: thesis: for o being OperSymbol of S st the_arity_of o <> {} holds
for y being Element of Args o,(product A)
for i' being Element of I
for g being Function st g = (Den o,(product A)) . y holds
g . i' = (Den o,(A . i')) . ((commute y) . i')
let o be OperSymbol of S; :: thesis: ( the_arity_of o <> {} implies for y being Element of Args o,(product A)
for i' being Element of I
for g being Function st g = (Den o,(product A)) . y holds
g . i' = (Den o,(A . i')) . ((commute y) . i') )
assume A1: the_arity_of o <> {} ; :: thesis: for y being Element of Args o,(product A)
for i' being Element of I
for g being Function st g = (Den o,(product A)) . y holds
g . i' = (Den o,(A . i')) . ((commute y) . i')
let y be Element of Args o,(product A); :: thesis: for i' being Element of I
for g being Function st g = (Den o,(product A)) . y holds
g . i' = (Den o,(A . i')) . ((commute y) . i')
let i' be Element of I; :: thesis: for g being Function st g = (Den o,(product A)) . y holds
g . i' = (Den o,(A . i')) . ((commute y) . i')
let g be Function; :: thesis: ( g = (Den o,(product A)) . y implies g . i' = (Den o,(A . i')) . ((commute y) . i') )
assume A2: g = (Den o,(product A)) . y ; :: thesis: g . i' = (Den o,(A . i')) . ((commute y) . i')
A3: Den o,(product A) = (OPS A) . o by MSUALG_1:def 11
.= IFEQ (the_arity_of o),{} ,(commute (A ?. o)),(Commute (Frege (A ?. o))) by PRALG_2:def 20
.= Commute (Frege (A ?. o)) by A1, FUNCOP_1:def 8 ;
A4: y in dom (Commute (Frege (A ?. o))) by A1, Th19;
A5: commute y in product (doms (A ?. o)) by A1, Th18;
A6: dom (A ?. o) = I by PARTFUN1:def 4;
g = (Frege (A ?. o)) . (commute y) by A2, A3, A4, PRALG_2:def 6
.= (A ?. o) .. (commute y) by A5, PRALG_2:def 8 ;
then g . i' = ((A ?. o) . i') . ((commute y) . i') by A6, PRALG_1:def 17
.= (Den o,(A . i')) . ((commute y) . i') by PRALG_2:14 ;
hence g . i' = (Den o,(A . i')) . ((commute y) . i') ; :: thesis: verum