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 A1: ( a in C + & b in C + ) ; :: thesis: a ^ b in C +
then consider k being Nat such that
A2: ( k > 0 & a in C |^ k ) by Th48;
consider l being Nat such that
A3: ( l > 0 & b in C |^ l ) by A1, Th48;
A4: k + l > 0 by A2;
a ^ b in C |^ (k + l) by A2, A3, FLANG_1:41;
hence a ^ b in C + by A4, Th48; :: thesis: verum