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

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 & c in L \/ M & a = b \/ c ) by Th15;
K ^ (L \/ M) c= PFuncs V,C by FINSUB_1:def 5;
then reconsider a' = 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 b' = b, c' = c as Element of PFuncs V,C by A2;
( b' c= a' & c' c= a' ) by A2, XBOOLE_1:7;
then A3: b' tolerates c' by PARTFUN1:139;
( c' in L or c' in M ) by A2, XBOOLE_0:def 3;
then ( a in K ^ L or a in K ^ M ) by A2, A3;
hence a in (K ^ L) \/ (K ^ M) by XBOOLE_0:def 3; :: thesis: verum

end;

hence K ^ (L \/ M) c= (K ^ L) \/ (K ^ M) by Lm2; :: 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