let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of the carrier of S
for o being OperSymbol of S
for p being FinSequence of TS () holds
( p in ((() #) * the Arity of S) . o iff ( dom p = dom () & ( for n being Nat st n in dom p holds
p . n in FreeSort (X,(() /. n)) ) ) )

let X be V5() ManySortedSet of the carrier of S; :: thesis: for o being OperSymbol of S
for p being FinSequence of TS () holds
( p in ((() #) * the Arity of S) . o iff ( dom p = dom () & ( for n being Nat st n in dom p holds
p . n in FreeSort (X,(() /. n)) ) ) )

let o be OperSymbol of S; :: thesis: for p being FinSequence of TS () holds
( p in ((() #) * the Arity of S) . o iff ( dom p = dom () & ( for n being Nat st n in dom p holds
p . n in FreeSort (X,(() /. n)) ) ) )

let p be FinSequence of TS (); :: thesis: ( p in ((() #) * the Arity of S) . o iff ( dom p = dom () & ( for n being Nat st n in dom p holds
p . n in FreeSort (X,(() /. n)) ) ) )

set AR = the Arity of S;
set cr = the carrier of S;
set ar = the_arity_of o;
thus ( p in ((() #) * the Arity of S) . o implies ( dom p = dom () & ( for n being Nat st n in dom p holds
p . n in FreeSort (X,(() /. n)) ) ) ) :: thesis: ( dom p = dom () & ( for n being Nat st n in dom p holds
p . n in FreeSort (X,(() /. n)) ) implies p in ((() #) * the Arity of S) . o )
proof
A1: the Arity of S . o = the_arity_of o by MSUALG_1:def 1;
A2: ( rng () c= the carrier of S & dom () = the carrier of S ) by ;
then A3: dom (() * ()) = dom () by RELAT_1:27;
assume p in ((() #) * the Arity of S) . o ; :: thesis: ( dom p = dom () & ( for n being Nat st n in dom p holds
p . n in FreeSort (X,(() /. n)) ) )

then A4: p in product (() * ()) by ;
then A5: dom p = dom (() * ()) by CARD_3:9;
hence dom p = dom () by ; :: thesis: for n being Nat st n in dom p holds
p . n in FreeSort (X,(() /. n))

let n be Nat; :: thesis: ( n in dom p implies p . n in FreeSort (X,(() /. n)) )
assume A6: n in dom p ; :: thesis: p . n in FreeSort (X,(() /. n))
then (() * ()) . n = () . (() . n) by
.= () . (() /. n) by
.= FreeSort (X,(() /. n)) by Def11 ;
hence p . n in FreeSort (X,(() /. n)) by ; :: thesis: verum
end;
assume that
A7: dom p = dom () and
A8: for n being Nat st n in dom p holds
p . n in FreeSort (X,(() /. n)) ; :: thesis: p in ((() #) * the Arity of S) . o
( rng () c= the carrier of S & dom () = the carrier of S ) by ;
then A9: dom p = dom (() * ()) by ;
A10: for x being object st x in dom (() * ()) holds
p . x in (() * ()) . x
proof
let x be object ; :: thesis: ( x in dom (() * ()) implies p . x in (() * ()) . x )
assume A11: x in dom (() * ()) ; :: thesis: p . x in (() * ()) . x
then reconsider n = x as Nat ;
FreeSort (X,(() /. n)) = () . (() /. n) by Def11
.= () . (() . n) by
.= (() * ()) . x by ;
hence p . x in (() * ()) . x by A8, A9, A11; :: thesis: verum
end;
the Arity of S . o = the_arity_of o by MSUALG_1:def 1;
then (((FreeSort X) #) * the Arity of S) . o = product (() * ()) by Th1;
hence p in ((() #) * the Arity of S) . o by ; :: thesis: verum