let B, C be set ; :: thesis: for P being Relation holds P * [:B,C:] c= [:(P " B),C:]
let P be Relation; :: thesis: P * [:B,C:] c= [:(P " B),C:]
set A = P " B;
set R1 = [:B,C:];
set R2 = [:(P " B),C:];
set Q = P * [:B,C:];
A1: (dom [:B,C:]) \ B = {} ;
dom (P * [:B,C:]) = P " (dom [:B,C:]) by RELAT_1:147;
then reconsider DQ = dom (P * [:B,C:]) as Subset of (P " B) by A1, Th29, RELAT_1:143;
[:DQ,C:] \ [:((P " B) \/ DQ),(C \/ {}):] = {} ;
then A2: [:DQ,C:] c= [:(P " B),C:] by Th29;
reconsider PP = P as Relation of (dom P),(rng P) by RELAT_1:7;
[:B,C:] c= [:B,C:] ;
then reconsider RR1 = [:B,C:] as Relation of B,C ;
reconsider QQ = PP * RR1 as Relation of (dom P),C ;
( [:(dom (P * [:B,C:])),(rng (P * [:B,C:])):] c= [:(dom (P * [:B,C:])),C:] & P * [:B,C:] c= [:(dom (P * [:B,C:])),(rng (P * [:B,C:])):] ) by RELAT_1:7, ZFMISC_1:95;
then P * [:B,C:] c= [:(dom (P * [:B,C:])),C:] ;
hence P * [:B,C:] c= [:(P " B),C:] by A2; :: thesis: verum