let X be set ; :: thesis: for I, f being Function holds (f | X) * I = (f * I) | (I " X)
let I, f be Function; :: thesis: (f | X) * I = (f * I) | (I " X)
P1: dom ((f | X) * I) = I " (dom (f | X)) by RELAT_1:147;
P2: I " (dom (f | X)) = I " ((dom f) /\ X) by RELAT_1:61
.= (I " (dom f)) /\ (I " X) by FUNCT_1:68
.= (dom (f * I)) /\ (I " X) by RELAT_1:147
.= dom ((f * I) | (I " X)) by RELAT_1:61 ;

now :: thesis: for x being object st x in dom ((f | X) * I) holds
((f | X) * I) . x = ((f * I) | (I " X)) . x

let x be object ; :: thesis: ( x in dom ((f | X) * I) implies ((f | X) * I) . x = ((f * I) | (I " X)) . x )
assume Q1: x in dom ((f | X) * I) ; :: thesis: ((f | X) * I) . x = ((f * I) | (I " X)) . x
then x in I " (dom (f | X)) by RELAT_1:147;
then Q3: ( x in dom I & I . x in dom (f | X) ) by FUNCT_1:def 7;
thus ((f | X) * I) . x = (f | X) . (I . x) by FUNCT_1:12, Q1
.= f . (I . x) by FUNCT_1:47, Q3
.= (f * I) . x by FUNCT_1:13, Q3
.= ((f * I) | (I " X)) . x by FUNCT_1:47, Q1, P1, P2 ; :: thesis: verum

end;

hence (f | X) * I = (f * I) | (I " X) by P2, FUNCT_1:2, RELAT_1:147; :: thesis: verum