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 } ) );
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 ) )
thus ( S <> {} & S₁[f] & S₁[g] implies f = g ) :: thesis: ( not S <> {} & f = {} & g = {} implies f = g )

proof

assume A4: ( S <> {} & S₁[f] & S₁[g] ) ; :: thesis: f = g
then 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 } ;
consider B being non empty functional set such that
A8: B = S and
A9: dom g = meet { (dom x) where x is Element of B : verum } and
A10: for i being set st i in dom g holds
g . i = { (x . i) where x is Element of B : verum } by A4;

now

let a be set ; :: thesis: ( a in meet { (dom x) where x is Element of A : verum } implies f . a = g . a )
assume A11: 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 A5, A8, A9, A10, A11 ;
:: thesis: verum

end;

hence f = g by A5, A6, A8, A9, FUNCT_1:9; :: thesis: verum

end;

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