let DK, DX be non empty set ; :: thesis:
let f be BinOp of DK; :: thesis:
assume that
A1: ( f is commutative & f is associative ) and
A2: f is having_a_unity ; :: thesis:
let Y1, Y2 be finite Subset of DX; :: thesis:
assume A3: Y1 misses Y2 ; :: thesis:
let F be Function of DX,DK; :: thesis:
assume that
A4: Y1 c= dom F and
A5: Y2 c= dom F ; :: thesis:
let Z be finite Subset of DX; :: thesis:
assume A6: Z = Y1 \/ Y2 ; :: thesis:
then A7: Z c= dom F by A4, A5, XBOOLE_1:8;
consider p1 being FinSequence of DX such that
A8: p1 is one-to-one and
A9: rng p1 = Y1 and
A10: setopfunc Y1,DX,DK,F,f = f "**" (Func_Seq F,p1) by A1, A2, A4, Def5;
consider p2 being FinSequence of DX such that
A11: p2 is one-to-one and
A12: rng p2 = Y2 and
A13: setopfunc Y2,DX,DK,F,f = f "**" (Func_Seq F,p2) by A1, A2, A5, Def5;
set q = p1 ^ p2;
A14: p1 ^ p2 is one-to-one by A3, A8, A9, A11, A12, FINSEQ_3:98;
rng (p1 ^ p2) = Z by A6, A9, A12, FINSEQ_1:44;
then A15: setopfunc Z,DX,DK,F,f = f "**" (Func_Seq F,(p1 ^ p2)) by A1, A2, A7, A14, Def5;
ex fp1, fp2 being FinSequence st
( fp1 = F * p1 & fp2 = F * p2 & F * (p1 ^ p2) = fp1 ^ fp2 ) by A4, A5, A6, A9, A12, HILBASIS:1, XBOOLE_1:8;
hence setopfunc Z,DX,DK,F,f = f . (setopfunc Y1,DX,DK,F,f),(setopfunc Y2,DX,DK,F,f) by A1, A2, A10, A13, A15, FINSOP_1:6; :: thesis: