let f, g be Relation; :: thesis: for A, B being set st A c= B & f | B = g | B holds
f | A = g | A
let A, B be set ; :: thesis: ( A c= B & f | B = g | B implies f | A = g | A )
assume that
A1: A c= B and
A2: f | B = g | B ; :: thesis: f | A = g | A
A3: A = B /\ A by A1, XBOOLE_1:28;
hence f | A = (f | B) | A by Th65
.= g | A by A2, A3, Th65 ;
:: thesis: verum