let B, C be set ; for P being Relation holds P * [:B,C:] c= [:(P " B),C:]
let P be Relation; 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; verum