let f be SetSequence of X; :: thesis: ( f = superior_setsequence A iff for n being Nat holds f . n = Union (A ^\ n) )
thus ( f = superior_setsequence A implies for n being Nat holds f . n = Union (A ^\ n) ) by Lemacik0; :: thesis: ( ( for n being Nat holds f . n = Union (A ^\ n) ) implies f = superior_setsequence A )
assume A1: for n being Nat holds f . n = Union (A ^\ n) ; :: thesis: f = superior_setsequence A
for n being Element of NAT holds f . n = (superior_setsequence A) . n
proof
let n be Element of NAT ; :: thesis: f . n = (superior_setsequence A) . n
f . n = Union (A ^\ n) by A1
.= (superior_setsequence A) . n by Lemacik0 ;
hence f . n = (superior_setsequence A) . n ; :: thesis: verum
end;
hence f = superior_setsequence A by FUNCT_2:def 8; :: thesis: verum