let B, C be set ; :: thesis: for P being Relation holds P * [:B,C:] = [:(P " B),C:]
let P be Relation; :: thesis: P * [:B,C:] = [:(P " B),C:]
set A = P " B;
set R1 = [:B,C:];
set R2 = [:(P " B),C:];
set Q = P * [:B,C:];
set LH = P * [:B,C:];
set RH = [:(P " B),C:];

now :: thesis: for z being object st z in [:(P " B),C:] holds
z in P * [:B,C:]

let z be object ; :: thesis: ( z in [:(P " B),C:] implies z in P * [:B,C:] )
assume z in [:(P " B),C:] ; :: thesis: z in P * [:B,C:]
then consider x, y being object such that
A1: ( x in P " B & y in C & z = [x,y] ) by ZFMISC_1:def 2;
consider x1 being object such that
A2: ( [x,x1] in P & x1 in B ) by RELAT_1:def 14, A1;
[x1,y] in [:B,C:] by A1, A2, ZFMISC_1:def 2;
hence z in P * [:B,C:] by A1, A2, RELAT_1:def 8; :: thesis: verum

end;

then ( [:(P " B),C:] c= P * [:B,C:] & P * [:B,C:] c= [:(P " B),C:] ) by Lm60;
hence P * [:B,C:] = [:(P " B),C:] ; :: thesis: verum