let E be set ; :: thesis: for C being Subset of (E ^omega)
for a, b being Element of E ^omega st a in C * & b in C * holds
a ^ b in C *
let C be Subset of (E ^omega); :: thesis: for a, b being Element of E ^omega st a in C * & b in C * holds
a ^ b in C *
let a, b be Element of E ^omega ; :: thesis: ( a in C * & b in C * implies a ^ b in C * )
assume that
A1: a in C * and
A2: b in C * ; :: thesis: a ^ b in C *
consider k being Nat such that
A3: a in C |^ k by A1, Th41;
consider l being Nat such that
A4: b in C |^ l by A2, Th41;
a ^ b in C |^ (k + l) by A3, A4, Th40;
hence a ^ b in C * by Th41; :: thesis: verum