let T, S be set ; :: thesis: for f being Function of T,S
for G being Subset-Family of T holds f .: G = { (f .: A) where A is Subset of T : A in G }
let f be Function of T,S; :: thesis: for G being Subset-Family of T holds f .: G = { (f .: A) where A is Subset of T : A in G }
let G be Subset-Family of T; :: thesis: f .: G = { (f .: A) where A is Subset of T : A in G }

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { (f .: A) where A is Subset of T : A in G } c= f .: G

let t be object ; :: thesis: ( t in f .: G implies t in { (f .: A) where A is Subset of T : A in G } )
assume A1: t in f .: G ; :: thesis: t in { (f .: A) where A is Subset of T : A in G }
then reconsider t1 = t as Subset of S ;
consider B being Subset of T such that
A2: B in G and
A3: t1 = f .: B by A1, FUNCT_2:def 10;
thus t in { (f .: A) where A is Subset of T : A in G } by A2, A3; :: thesis: verum

end;

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { (f .: A) where A is Subset of T : A in G } or t in f .: G )
assume t in { (f .: A) where A is Subset of T : A in G } ; :: thesis: t in f .: G
then consider A being Subset of T such that
A4: t = f .: A and
A5: A in G ;
thus t in f .: G by A4, A5, FUNCT_2:def 10; :: thesis: verum