let X be set ; :: thesis: for F being Domain-Sequence

for p being FinSequence holds

( p is MultOps of X,F iff ( len p = len F & ( for i being set st i in dom F holds

p . i is Function of [:X,(F . i):],(F . i) ) ) )

let F be Domain-Sequence; :: thesis: for p being FinSequence holds

( p is MultOps of X,F iff ( len p = len F & ( for i being set st i in dom F holds

p . i is Function of [:X,(F . i):],(F . i) ) ) )

let p be FinSequence; :: thesis: ( p is MultOps of X,F iff ( len p = len F & ( for i being set st i in dom F holds

p . i is Function of [:X,(F . i):],(F . i) ) ) )

( dom p = dom F iff len p = len F ) by FINSEQ_3:29;

hence ( p is MultOps of X,F iff ( len p = len F & ( for i being set st i in dom F holds

p . i is Function of [:X,(F . i):],(F . i) ) ) ) by Def1; :: thesis: verum

for p being FinSequence holds

( p is MultOps of X,F iff ( len p = len F & ( for i being set st i in dom F holds

p . i is Function of [:X,(F . i):],(F . i) ) ) )

let F be Domain-Sequence; :: thesis: for p being FinSequence holds

( p is MultOps of X,F iff ( len p = len F & ( for i being set st i in dom F holds

p . i is Function of [:X,(F . i):],(F . i) ) ) )

let p be FinSequence; :: thesis: ( p is MultOps of X,F iff ( len p = len F & ( for i being set st i in dom F holds

p . i is Function of [:X,(F . i):],(F . i) ) ) )

( dom p = dom F iff len p = len F ) by FINSEQ_3:29;

hence ( p is MultOps of X,F iff ( len p = len F & ( for i being set st i in dom F holds

p . i is Function of [:X,(F . i):],(F . i) ) ) ) by Def1; :: thesis: verum