let V, C be set ; :: thesis: for K, L, M being Element of Fin (PFuncs (V,C)) holds K ^ (L \/ M) = (K ^ L) \/ (K ^ M)
let K, L, M be Element of Fin (PFuncs (V,C)); :: thesis: K ^ (L \/ M) = (K ^ L) \/ (K ^ M)

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

let a be set ; :: thesis: ( a in K ^ (L \/ M) implies a in (K ^ L) \/ (K ^ M) )
assume A1: a in K ^ (L \/ M) ; :: thesis: a in (K ^ L) \/ (K ^ M)
then consider b, c being set such that
A2: b in K and
A3: c in L \/ M and
A4: a = b \/ c by Th15;
K ^ (L \/ M) c= PFuncs (V,C) by FINSUB_1:def 5;
then reconsider a9 = a as Element of PFuncs (V,C) by A1;
( K c= PFuncs (V,C) & L \/ M c= PFuncs (V,C) ) by FINSUB_1:def 5;
then reconsider b9 = b, c9 = c as Element of PFuncs (V,C) by A2, A3;
( b9 c= a9 & c9 c= a9 ) by A4, XBOOLE_1:7;
then A5: b9 tolerates c9 by PARTFUN1:57;
( c9 in L or c9 in M ) by A3, XBOOLE_0:def 3;
then ( a in K ^ L or a in K ^ M ) by A2, A4, A5;
hence a in (K ^ L) \/ (K ^ M) by XBOOLE_0:def 3; :: thesis: verum

end;

hence K ^ (L \/ M) c= (K ^ L) \/ (K ^ M) ; :: according to XBOOLE_0:def 10 :: thesis: (K ^ L) \/ (K ^ M) c= K ^ (L \/ M)
( K ^ L c= K ^ (L \/ M) & K ^ M c= K ^ (L \/ M) ) by Th18, XBOOLE_1:7;
hence (K ^ L) \/ (K ^ M) c= K ^ (L \/ M) by XBOOLE_1:8; :: thesis: verum