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:
( (K ^ L) ^ M = M ^ (K ^ L) & K ^ (L ^ M) = (L ^ M) ^ K & L ^ M = M ^ L & K ^ L = L ^ K )
by Th3;
now let K,
L,
M be
Element of
Fin (PFuncs V,C);
:: thesis: K ^ (L ^ M) c= (K ^ L) ^ MA2:
(
K c= PFuncs V,
C &
L c= PFuncs V,
C &
M c= PFuncs V,
C )
by FINSUB_1:def 5;
now let a be
set ;
:: thesis: ( a in K ^ (L ^ M) implies a in (K ^ L) ^ M )assume A3:
a in K ^ (L ^ M)
;
:: thesis: a in (K ^ L) ^ Mthen consider b,
c being
set such that A4:
b in K
and A5:
c in L ^ M
and A6:
a = b \/ c
by Th15;
K ^ (L ^ M) c= PFuncs V,
C
by FINSUB_1:def 5;
then consider f being
Function such that A7:
(
a = f &
dom f c= V &
rng f c= C )
by A3, PARTFUN1:def 5;
consider b1,
c1 being
set such that A8:
b1 in L
and A9:
c1 in M
and A10:
c = b1 \/ c1
by A5, Th15;
reconsider b' =
b,
b1' =
b1,
c1' =
c1 as
Element of
PFuncs V,
C by A2, A4, A8, A9;
reconsider b2 =
b,
b12 =
b1 as
PartFunc of
V,
C by A2, A4, A8, PARTFUN1:120;
A11:
(
b c= b \/ c &
c c= b \/ c )
by XBOOLE_1:7;
b1 c= c
by A10, XBOOLE_1:7;
then A12:
b1 c= b \/ c
by A11, XBOOLE_1:1;
then A13:
b' tolerates b1'
by A6, A7, A11, PARTFUN1:139;
A14:
b \/ (b1 \/ c1) = (b \/ b1) \/ c1
by XBOOLE_1:4;
b' \/ b1' = b' +* b1'
by A13, FUNCT_4:31;
then
b2 \/ b12 is
PartFunc of
V,
C
;
then reconsider c2 =
b' \/ b1' as
Element of
PFuncs V,
C by PARTFUN1:119;
A15:
c2 in K ^ L
by A4, A8, A13;
c1 c= c
by A10, XBOOLE_1:7;
then A16:
c1 c= b \/ c
by A11, XBOOLE_1:1;
c2 c= b \/ c
by A11, A12, XBOOLE_1:8;
then
c2 tolerates c1'
by A6, A7, A16, PARTFUN1:139;
hence
a in (K ^ L) ^ M
by A6, A9, A10, A14, A15;
:: thesis: verum end; hence
K ^ (L ^ M) c= (K ^ L) ^ M
by Lm2;
:: thesis: verum end;
then
( (K ^ L) ^ M c= K ^ (L ^ M) & K ^ (L ^ M) c= (K ^ L) ^ M )
by A1;
hence
K ^ (L ^ M) = (K ^ L) ^ M
by XBOOLE_0:def 10; :: thesis: verum