let A1, A2 be Subset of X; :: thesis: ( ex f being SetSequence of X st
( A1 = Union f & ( for n being Nat holds f . n = meet (F ^\ n) ) ) & ex f being SetSequence of X st
( A2 = Union f & ( for n being Nat holds f . n = meet (F ^\ n) ) ) implies A1 = A2 )
given f1 being SetSequence of X such that A2: A1 = Union f1 and
A3: for n being Nat holds f1 . n = meet (F ^\ n) ; :: thesis: ( for f being SetSequence of X holds
( not A2 = Union f or ex n being Nat st not f . n = meet (F ^\ n) ) or A1 = A2 )
given f2 being SetSequence of X such that A4: A2 = Union f2 and
A5: for n being Nat holds f2 . n = meet (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 = meet (F ^\ n) by A3
.= f2 . n by A5 ;
hence f1 . n = f2 . n ; :: thesis: verum

end;

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