let D be non empty set ; :: thesis: for p, q being FinSequence of D
for B being BinOp of D st p is one-to-one & q is one-to-one & rng q c= rng p & B is commutative & B is associative & ( B is having_a_unity or ( len q >= 1 & len p > len q ) ) holds
ex r being FinSequence of D st
( r is one-to-one & rng r = (rng p) \ (rng q) & B "**" p = B . ((B "**" q),(B "**" r)) )

let p, q be FinSequence of D; :: thesis: for B being BinOp of D st p is one-to-one & q is one-to-one & rng q c= rng p & B is commutative & B is associative & ( B is having_a_unity or ( len q >= 1 & len p > len q ) ) holds
ex r being FinSequence of D st
( r is one-to-one & rng r = (rng p) \ (rng q) & B "**" p = B . ((B "**" q),(B "**" r)) )

let B be BinOp of D; :: thesis: ( p is one-to-one & q is one-to-one & rng q c= rng p & B is commutative & B is associative & ( B is having_a_unity or ( len q >= 1 & len p > len q ) ) implies ex r being FinSequence of D st
( r is one-to-one & rng r = (rng p) \ (rng q) & B "**" p = B . ((B "**" q),(B "**" r)) ) )

assume that
A1: p is one-to-one and
A2: q is one-to-one and
A3: rng q c= rng p and
A4: ( B is commutative & B is associative ) and
A5: ( B is having_a_unity or ( len q >= 1 & len p > len q ) ) ; :: thesis: ex r being FinSequence of D st
( r is one-to-one & rng r = (rng p) \ (rng q) & B "**" p = B . ((B "**" q),(B "**" r)) )

A6: card (rng p) = len p by ;
consider r being FinSequence such that
A7: rng r = (rng p) \ (rng q) and
A8: r is one-to-one by FINSEQ_4:58;
reconsider r = r as FinSequence of D by ;
rng (q ^ r) = (rng q) \/ ((rng p) \ (rng q)) by ;
then A9: rng (q ^ r) = rng p by ;
rng r misses rng q by ;
then A10: q ^ r is one-to-one by ;
then card (rng (q ^ r)) = len (q ^ r) by FINSEQ_4:62;
then ( len q < (len q) + (len r) or B is having_a_unity ) by ;
then A11: ( ( 1 <= len r & 1 <= len q & 1 <= len p ) or B is having_a_unity ) by ;
ex P being Permutation of (dom p) st
( p * P = q ^ r & dom P = dom p & rng P = dom p ) by ;
then A12: B "**" p = B "**" (q ^ r) by ;
B "**" (q ^ r) = B . ((B "**" q),(B "**" r)) by ;
hence ex r being FinSequence of D st
( r is one-to-one & rng r = (rng p) \ (rng q) & B "**" p = B . ((B "**" q),(B "**" r)) ) by A7, A8, A12; :: thesis: verum