let i be set ; :: thesis: for f being Function st i in dom f holds
|.{f}.| . i = {(f . i)}
let f be Function; :: thesis: ( i in dom f implies |.{f}.| . i = {(f . i)} )
A1: f in {f} by TARSKI:def 1;
consider A being non empty functional set such that
A2: A = {f} and
dom |.{f}.| = meet { (dom x) where x is Element of A : verum } and
A3: for i being set st i in dom |.{f}.| holds
|.{f}.| . i = { (x . i) where x is Element of A : verum } by Def2;
assume i in dom f ; :: thesis: |.{f}.| . i = {(f . i)}
then i in dom |.{f}.| by Th15;
then A4: |.{f}.| . i = { (x . i) where x is Element of A : verum } by A3;
thus |.{f}.| . i c= {(f . i)} :: according to XBOOLE_0:def 10 :: thesis: {(f . i)} c= |.{f}.| . i
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in |.{f}.| . i or q in {(f . i)} )
assume q in |.{f}.| . i ; :: thesis: q in {(f . i)}
then consider x being Element of A such that
A5: q = x . i by A4;
x = f by A2, TARSKI:def 1;
hence q in {(f . i)} by A5, TARSKI:def 1; :: thesis: verum
end;
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in {(f . i)} or q in |.{f}.| . i )
assume q in {(f . i)} ; :: thesis: q in |.{f}.| . i
then q = f . i by TARSKI:def 1;
hence q in |.{f}.| . i by A2, A4, A1; :: thesis: verum