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 & q is one-to-one & rng q c= rng p ) and
A2: ( B is commutative & B is associative & ( 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) )
consider r being FinSequence such that
A3: ( rng r = (rng p) \ (rng q) & r is one-to-one ) by FINSEQ_4:73;
reconsider r = r as FinSequence of D by A3, FINSEQ_1:def 4;
( rng r misses rng q & rng (q ^ r) = (rng q) \/ ((rng p) \ (rng q)) ) by A3, FINSEQ_1:44, XBOOLE_1:79;
then A4: ( q ^ r is one-to-one & rng (q ^ r) = rng p ) by A1, A3, FINSEQ_3:98, XBOOLE_1:45;
then consider P being Permutation of (dom p) such that
A5: ( p * P = q ^ r & dom P = dom p & rng P = dom p ) by A1, BHSP_5:1;
( card (rng p) = len p & card (rng (q ^ r)) = len (q ^ r) ) by A1, A4, FINSEQ_4:77;
then ( len q < (len q) + (len r) or B is having_a_unity ) by A2, A4, FINSEQ_1:35;
then ( ( 1 <= len r & 1 <= len q & 1 <= len p ) or B is having_a_unity ) by A2, NAT_1:19, XXREAL_0:2;
then ( B "**" (q ^ r) = B . (B "**" q),(B "**" r) & B "**" p = B "**" (q ^ r) ) by A2, A5, FINSOP_1:6, FINSOP_1:8;
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 A3; :: thesis: verum