let D be set ; :: thesis: for p, q being Element of D * holds FlattenSeq <*p,q*> = p ^ q
let p, q be Element of D * ; :: thesis: FlattenSeq <*p,q*> = p ^ q
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*> = g "**" <*p,q*> by Def14;
thus FlattenSeq <*p,q*> = g . p,q by A2, FINSOP_1:13
.= p ^ q by A1 ; :: thesis: verum