let D be set ; :: thesis: for p, q, r being Element of D * holds FlattenSeq <*p,q,r*> = (p ^ q) ^ r
let p, q, r be Element of D * ; :: thesis: FlattenSeq <*p,q,r*> = (p ^ q) ^ r
consider g being BinOp of (D *) such that
A1: for d1, d2 being Element of D * holds g . (d1,d2) = d1 ^ d2 and
A2: FlattenSeq <*p,q,r*> = g "**" <*p,q,r*> by Def1;
thus FlattenSeq <*p,q,r*> = g . ((g . (p,q)),r) by A2, FINSOP_1:14
.= (g . (p,q)) ^ r by A1
.= (p ^ q) ^ r by A1 ; :: thesis: verum