{ (f |^ i) where i is Nat : verum } c= the carrier of A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (f |^ i) where i is Nat : verum } or x in the carrier of A )
assume x in { (f |^ i) where i is Nat : verum } ; :: thesis: x in the carrier of A
then consider k being Nat such that
A2: x = f |^ k ;
thus x in the carrier of A by A2; :: thesis: verum

end;

hence { (f |^ i) where i is Nat : verum } is Subset of A ; :: thesis: verum