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