let i be set ; :: thesis: for f, f1 being Function st i in dom |.{f,f1}.| holds
|.{f,f1}.| . i = {(f . i),(f1 . i)}
let f, f1 be Function; :: thesis: ( i in dom |.{f,f1}.| implies |.{f,f1}.| . i = {(f . i),(f1 . i)} )
A1: ( f in {f,f1} & f1 in {f,f1} ) by TARSKI:def 2;
consider A being non empty functional set such that
A2: A = {f,f1} and
dom |.{f,f1}.| = meet { (dom x) where x is Element of A : verum } and
A3: for i being set st i in dom |.{f,f1}.| holds
|.{f,f1}.| . i = { (x . i) where x is Element of A : verum } by Def2;
assume i in dom |.{f,f1}.| ; :: thesis: |.{f,f1}.| . i = {(f . i),(f1 . i)}
then A4: |.{f,f1}.| . i = { (x . i) where x is Element of A : verum } by A3;
thus |.{f,f1}.| . i c= {(f . i),(f1 . i)} :: according to XBOOLE_0:def 10 :: thesis: {(f . i),(f1 . i)} c= |.{f,f1}.| . i

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in |.{f,f1}.| . i or q in {(f . i),(f1 . i)} )
assume q in |.{f,f1}.| . i ; :: thesis: q in {(f . i),(f1 . i)}
then consider x being Element of A such that
A5: q = x . i by A4;

per cases ( x = f or x = f1 ) by A2, TARSKI:def 2;

suppose x = f ; :: thesis: q in {(f . i),(f1 . i)}

hence q in {(f . i),(f1 . i)} by A5, TARSKI:def 2; :: thesis: verum

end;

suppose x = f1 ; :: thesis: q in {(f . i),(f1 . i)}

hence q in {(f . i),(f1 . i)} by A5, TARSKI:def 2; :: thesis: verum

end;

end;

end;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in {(f . i),(f1 . i)} or q in |.{f,f1}.| . i )
assume q in {(f . i),(f1 . i)} ; :: thesis: q in |.{f,f1}.| . i
then ( q = f . i or q = f1 . i ) by TARSKI:def 2;
hence q in |.{f,f1}.| . i by A2, A4, A1; :: thesis: verum