let A1, A2 be Subset of X; :: thesis: ( ex f being SetSequence of X st
( A1 = meet f & ( for n being Nat holds f . n = Union (F ^\ n) ) ) & ex f being SetSequence of X st
( A2 = meet f & ( for n being Nat holds f . n = Union (F ^\ n) ) ) implies A1 = A2 )
given f1 being SetSequence of X such that A7: A1 = meet f1 and
A8: for n being Nat holds f1 . n = Union (F ^\ n) ; :: thesis: ( for f being SetSequence of X holds
( not A2 = meet f or ex n being Nat st not f . n = Union (F ^\ n) ) or A1 = A2 )
given f2 being SetSequence of X such that A9: A2 = meet f2 and
A10: for n being Nat holds f2 . n = Union (F ^\ n) ; :: thesis: A1 = A2
for n being Element of NAT holds f1 . n = f2 . n

proof

let n be Element of NAT ; :: thesis: f1 . n = f2 . n
f1 . n = Union (F ^\ n) by A8
.= f2 . n by A10 ;
hence f1 . n = f2 . n ; :: thesis: verum

end;

hence A1 = A2 by A7, A9, FUNCT_2:63; :: thesis: verum