let DK, DX be non empty set ; :: thesis: for f being BinOp of DK st f is commutative & f is associative & f is having_a_unity holds
for Y1, Y2 being finite Subset of DX st Y1 misses Y2 holds
for F being Function of DX,DK st Y1 c= dom F & Y2 c= dom F holds
for Z being finite Subset of DX st Z = Y1 \/ Y2 holds
setopfunc (Z,DX,DK,F,f) = f . ((setopfunc (Y1,DX,DK,F,f)),(setopfunc (Y2,DX,DK,F,f)))
let f be BinOp of DK; :: thesis: ( f is commutative & f is associative & f is having_a_unity implies for Y1, Y2 being finite Subset of DX st Y1 misses Y2 holds
for F being Function of DX,DK st Y1 c= dom F & Y2 c= dom F holds
for Z being finite Subset of DX st Z = Y1 \/ Y2 holds
setopfunc (Z,DX,DK,F,f) = f . ((setopfunc (Y1,DX,DK,F,f)),(setopfunc (Y2,DX,DK,F,f))) )
assume that
A1: ( f is commutative & f is associative ) and
A2: f is having_a_unity ; :: thesis: for Y1, Y2 being finite Subset of DX st Y1 misses Y2 holds
for F being Function of DX,DK st Y1 c= dom F & Y2 c= dom F holds
for Z being finite Subset of DX st Z = Y1 \/ Y2 holds
setopfunc (Z,DX,DK,F,f) = f . ((setopfunc (Y1,DX,DK,F,f)),(setopfunc (Y2,DX,DK,F,f)))
let Y1, Y2 be finite Subset of DX; :: thesis: ( Y1 misses Y2 implies for F being Function of DX,DK st Y1 c= dom F & Y2 c= dom F holds
for Z being finite Subset of DX st Z = Y1 \/ Y2 holds
setopfunc (Z,DX,DK,F,f) = f . ((setopfunc (Y1,DX,DK,F,f)),(setopfunc (Y2,DX,DK,F,f))) )
assume A3: Y1 misses Y2 ; :: thesis: for F being Function of DX,DK st Y1 c= dom F & Y2 c= dom F holds
for Z being finite Subset of DX st Z = Y1 \/ Y2 holds
setopfunc (Z,DX,DK,F,f) = f . ((setopfunc (Y1,DX,DK,F,f)),(setopfunc (Y2,DX,DK,F,f)))
let F be Function of DX,DK; :: thesis: ( Y1 c= dom F & Y2 c= dom F implies for Z being finite Subset of DX st Z = Y1 \/ Y2 holds
setopfunc (Z,DX,DK,F,f) = f . ((setopfunc (Y1,DX,DK,F,f)),(setopfunc (Y2,DX,DK,F,f))) )
assume that
A4: Y1 c= dom F and
A5: Y2 c= dom F ; :: thesis: for Z being finite Subset of DX st Z = Y1 \/ Y2 holds
setopfunc (Z,DX,DK,F,f) = f . ((setopfunc (Y1,DX,DK,F,f)),(setopfunc (Y2,DX,DK,F,f)))
let Z be finite Subset of DX; :: thesis: ( Z = Y1 \/ Y2 implies setopfunc (Z,DX,DK,F,f) = f . ((setopfunc (Y1,DX,DK,F,f)),(setopfunc (Y2,DX,DK,F,f))) )
assume A6: Z = Y1 \/ Y2 ; :: thesis: setopfunc (Z,DX,DK,F,f) = f . ((setopfunc (Y1,DX,DK,F,f)),(setopfunc (Y2,DX,DK,F,f)))
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, 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, Def5;
set q = p1 ^ p2;
A14: p1 ^ p2 is one-to-one by A3, A8, A9, A11, A12, FINSEQ_3:91;
rng (p1 ^ p2) = Z by A6, A9, A12, FINSEQ_1:31;
then A15: setopfunc (Z,DX,DK,F,f) = f "**" (Func_Seq (F,(p1 ^ p2))) by A1, A2, 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:5; :: thesis: verum