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 A1, FINSEQ_4:62;

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 A7, FINSEQ_1:def 4;

rng (q ^ r) = (rng q) \/ ((rng p) \ (rng q)) by A7, FINSEQ_1:31;

then A9: rng (q ^ r) = rng p by A3, XBOOLE_1:45;

rng r misses rng q by A7, XBOOLE_1:79;

then A10: q ^ r is one-to-one by A2, A8, FINSEQ_3:91;

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 A5, A9, A6, FINSEQ_1:22;

then A11: ( ( 1 <= len r & 1 <= len q & 1 <= len p ) or B is having_a_unity ) by A5, NAT_1:19, XXREAL_0:2;

ex P being Permutation of (dom p) st

( p * P = q ^ r & dom P = dom p & rng P = dom p ) by A1, A10, A9, BHSP_5:1;

then A12: B "**" p = B "**" (q ^ r) by A4, A11, FINSOP_1:7;

B "**" (q ^ r) = B . ((B "**" q),(B "**" r)) by A4, A11, FINSOP_1:5;

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

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 A1, FINSEQ_4:62;

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 A7, FINSEQ_1:def 4;

rng (q ^ r) = (rng q) \/ ((rng p) \ (rng q)) by A7, FINSEQ_1:31;

then A9: rng (q ^ r) = rng p by A3, XBOOLE_1:45;

rng r misses rng q by A7, XBOOLE_1:79;

then A10: q ^ r is one-to-one by A2, A8, FINSEQ_3:91;

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 A5, A9, A6, FINSEQ_1:22;

then A11: ( ( 1 <= len r & 1 <= len q & 1 <= len p ) or B is having_a_unity ) by A5, NAT_1:19, XXREAL_0:2;

ex P being Permutation of (dom p) st

( p * P = q ^ r & dom P = dom p & rng P = dom p ) by A1, A10, A9, BHSP_5:1;

then A12: B "**" p = B "**" (q ^ r) by A4, A11, FINSOP_1:7;

B "**" (q ^ r) = B . ((B "**" q),(B "**" r)) by A4, A11, FINSOP_1:5;

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