let A1, A2 be Subset of X; :: thesis:
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:
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:
for n being Element of NAT holds f1 . n = f2 . n

let n be Element of NAT ; :: thesis:
f1 . n = meet (F ^\ n) by A3
.= f2 . n by A5 ;
hence f1 . n = f2 . n ; :: thesis:

end;