let f, g be Function; :: thesis: ( ( S <> {} & ex A being non empty functional set st
( A = S & dom f = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom f holds
f . i = { (x . i) where x is Element of A : verum } ) ) & ex A being non empty functional set st
( A = S & dom g = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom g holds
g . i = { (x . i) where x is Element of A : verum } ) ) implies f = g ) & ( not S <> {} & f = {} & g = {} implies f = g ) )
defpred S₁[ Function] means ex A being non empty functional set st
( A = S & dom $1 = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom $1 holds
$1 . i = { (x . i) where x is Element of A : verum } ) );
thus ( S <> {} & S₁[f] & S₁[g] implies f = g ) :: thesis: ( not S <> {} & f = {} & g = {} implies f = g )

proof

assume that
S <> {} and
A3: S₁[f] and
A4: S₁[g] ; :: thesis: f = g
consider A being non empty functional set such that
A5: A = S and
A6: dom f = meet { (dom x) where x is Element of A : verum } and
A7: for i being set st i in dom f holds
f . i = { (x . i) where x is Element of A : verum } by A3;

now :: thesis: for a being object st a in meet { (dom x) where x is Element of A : verum } holds
f . a = g . a

let a be object ; :: thesis: ( a in meet { (dom x) where x is Element of A : verum } implies f . a = g . a )
assume A8: a in meet { (dom x) where x is Element of A : verum } ; :: thesis: f . a = g . a
hence f . a = { (x . a) where x is Element of A : verum } by A6, A7
.= g . a by A4, A5, A8 ;
:: thesis: verum

end;

hence f = g by A4, A5, A6; :: thesis: verum

end;

thus ( not S <> {} & f = {} & g = {} implies f = g ) ; :: thesis: verum