let x be object ; :: thesis: for f being Function st x in dom f & product f <> {} holds
pi ((product f),x) = f . x
let f be Function; :: thesis: ( x in dom f & product f <> {} implies pi ((product f),x) = f . x )
assume that
A1: x in dom f and
A2: product f <> {} ; :: thesis: pi ((product f),x) = f . x
A3: pi ((product f),x) c= f . x

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in pi ((product f),x) or y in f . x )
assume y in pi ((product f),x) ; :: thesis: y in f . x
then ex g being Function st
( g in product f & y = g . x ) by Def6;
hence y in f . x by A1, Th9; :: thesis: verum

end;

f . x c= pi ((product f),x)

proof

set z = the Element of product f;
consider g being Function such that
the Element of product f = g and
A4: dom g = dom f and
A5: for x being object st x in dom f holds
g . x in f . x by A2, Def5;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f . x or y in pi ((product f),x) )
reconsider yy = y as set by TARSKI:1;
deffunc H₁( object ) -> set = yy;
deffunc H₂( object ) -> set = g . $1;
defpred S₂[ object ] means x = $1;
consider h being Function such that
A6: ( dom h = dom g & ( for z being object st z in dom g holds
( ( S₂[z] implies h . z = H₁(z) ) & ( not S₂[z] implies h . z = H₂(z) ) ) ) ) from PARTFUN1:sch 1();
assume A7: y in f . x ; :: thesis: y in pi ((product f),x)

now :: thesis: for z being object st z in dom f holds
h . z in f . z

let z be object ; :: thesis: ( z in dom f implies h . z in f . z )
assume A8: z in dom f ; :: thesis: h . z in f . z
then ( x <> z implies g . z = h . z ) by A4, A6;
hence h . z in f . z by A4, A5, A6, A7, A8; :: thesis: verum

end;

then A9: h in product f by A4, A6, Th9;
h . x = y by A1, A4, A6;
hence y in pi ((product f),x) by A9, Def6; :: thesis: verum

end;

hence pi ((product f),x) = f . x by A3; :: thesis: verum