let V, C be set ; :: thesis: for K, L, M being Element of Fin (PFuncs (V,C)) holds K ^ (L ^ M) = (K ^ L) ^ M
let K, L, M be Element of Fin (PFuncs (V,C)); :: thesis: K ^ (L ^ M) = (K ^ L) ^ M
A1: ( L ^ M = M ^ L & K ^ L = L ^ K ) by Th3;

A2: now :: thesis: for K, L, M being Element of Fin (PFuncs (V,C)) holds K ^ (L ^ M) c= (K ^ L) ^ M

let K, L, M be Element of Fin (PFuncs (V,C)); :: thesis: K ^ (L ^ M) c= (K ^ L) ^ M
A3: ( K c= PFuncs (V,C) & L c= PFuncs (V,C) ) by FINSUB_1:def 5;
A4: M c= PFuncs (V,C) by FINSUB_1:def 5;

now :: thesis: for a being set st a in K ^ (L ^ M) holds
a in (K ^ L) ^ M

let a be set ; :: thesis: ( a in K ^ (L ^ M) implies a in (K ^ L) ^ M )
A5: K ^ (L ^ M) c= PFuncs (V,C) by FINSUB_1:def 5;
assume A6: a in K ^ (L ^ M) ; :: thesis: a in (K ^ L) ^ M
then consider b, c being set such that
A7: b in K and
A8: c in L ^ M and
A9: a = b \/ c by Th15;
A10: c c= b \/ c by XBOOLE_1:7;
consider b1, c1 being set such that
A11: b1 in L and
A12: c1 in M and
A13: c = b1 \/ c1 by A8, Th15;
reconsider b2 = b, b12 = b1 as PartFunc of V,C by A3, A7, A11, PARTFUN1:46;
reconsider b9 = b, b19 = b1, c19 = c1 as Element of PFuncs (V,C) by A3, A4, A7, A11, A12;
b1 c= c by A13, XBOOLE_1:7;
then A14: ( b c= b \/ c & b1 c= b \/ c ) by A10, XBOOLE_1:7;
then A15: b9 tolerates b19 by A6, A9, A5, PARTFUN1:57;
then b9 \/ b19 = b9 +* b19 by FUNCT_4:30;
then b2 \/ b12 is PartFunc of V,C ;
then reconsider c2 = b9 \/ b19 as Element of PFuncs (V,C) by PARTFUN1:45;
A16: ( b \/ (b1 \/ c1) = (b \/ b1) \/ c1 & c2 in K ^ L ) by A7, A11, A15, XBOOLE_1:4;
c1 c= c by A13, XBOOLE_1:7;
then A17: c1 c= b \/ c by A10;
c2 c= b \/ c by A14, XBOOLE_1:8;
then c2 tolerates c19 by A6, A9, A5, A17, PARTFUN1:57;
hence a in (K ^ L) ^ M by A9, A12, A13, A16; :: thesis: verum

end;

hence K ^ (L ^ M) c= (K ^ L) ^ M ; :: thesis: verum

end;

then A18: K ^ (L ^ M) c= (K ^ L) ^ M ;
( (K ^ L) ^ M = M ^ (K ^ L) & K ^ (L ^ M) = (L ^ M) ^ K ) by Th3;
then (K ^ L) ^ M c= K ^ (L ^ M) by A1, A2;
hence K ^ (L ^ M) = (K ^ L) ^ M by A18; :: thesis: verum