let X be set ; :: thesis: for f, g being Relation st dom g c= X & g c= f holds
g c= f | X
let f, g be Relation; :: thesis: ( dom g c= X & g c= f implies g c= f | X )
assume ( dom g c= X & g c= f ) ; :: thesis: g c= f | X
then g | (dom g) c= f | X by Th106;
hence g c= f | X by Th97; :: thesis: verum