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

( p is BinOps of a iff ( len p = len a & ( for i being Element of dom a holds p . i is BinOp of (a . i) ) ) )

let p be FinSequence; :: thesis: ( p is BinOps of a iff ( len p = len a & ( for i being Element of dom a holds p . i is BinOp of (a . i) ) ) )

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

hence ( p is BinOps of a iff ( len p = len a & ( for i being Element of dom a holds p . i is BinOp of (a . i) ) ) ) by Def6; :: thesis: verum

( p is BinOps of a iff ( len p = len a & ( for i being Element of dom a holds p . i is BinOp of (a . i) ) ) )

let p be FinSequence; :: thesis: ( p is BinOps of a iff ( len p = len a & ( for i being Element of dom a holds p . i is BinOp of (a . i) ) ) )

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

hence ( p is BinOps of a iff ( len p = len a & ( for i being Element of dom a holds p . i is BinOp of (a . i) ) ) ) by Def6; :: thesis: verum