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
y in dom (Commute (Frege (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
y in dom (Commute (Frege (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
y in dom (Commute (Frege (A ?. o)))
let o be OperSymbol of S; :: thesis: for y being Element of Args o,(product A) st the_arity_of o <> {} holds
y in dom (Commute (Frege (A ?. o)))
let y be Element of Args o,(product A); :: thesis: ( the_arity_of o <> {} implies y in dom (Commute (Frege (A ?. o))) )
assume A1: the_arity_of o <> {} ; :: thesis: y in dom (Commute (Frege (A ?. o)))
then commute y in product (doms (A ?. o)) by Th18;
then A2: commute y in dom (Frege (A ?. o)) by PARTFUN1:def 4;
set D = union { (the Sorts of (A . ii) . ss) where ii is Element of I, ss is Element of the carrier of S : verum } ;
A3: y in Funcs (dom (the_arity_of o)),(Funcs I,(union { (the Sorts of (A . ii) . ss) where ii is Element of I, ss is Element of the carrier of S : verum } )) by Th15;
dom (the_arity_of o) <> {} by A1;
then y = commute (commute y) by A3, FUNCT_6:87;
hence y in dom (Commute (Frege (A ?. o))) by A2, PRALG_2:def 6; :: thesis: verum