let S be 1-sorted ; :: thesis: for T being non empty 1-sorted
for f being Function of S,T
for X being Subset of T holds (f " X) ` = f " (X `)
let T be non empty 1-sorted ; :: thesis: for f being Function of S,T
for X being Subset of T holds (f " X) ` = f " (X `)
let f be Function of S,T; :: thesis: for X being Subset of T holds (f " X) ` = f " (X `)
let X be Subset of T; :: thesis: (f " X) ` = f " (X `)
thus (f " X) ` = the carrier of S \ (f " X) by SUBSET_1:def 4
.= (f " the carrier of T) \ (f " X) by FUNCT_2:40
.= f " ( the carrier of T \ X) by FUNCT_1:69
.= f " (X `) by SUBSET_1:def 4 ; :: thesis: verum