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 l being Nat such that

l > 0 and

A3: b in C |^ l by A2, Th48;

consider k being Nat such that

A4: k > 0 and

A5: a in C |^ k by A1, Th48;

a ^ b in C |^ (k + l) by A5, A3, FLANG_1:40;

hence a ^ b in C + by A4, Th48; :: thesis: verum

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 l being Nat such that

l > 0 and

A3: b in C |^ l by A2, Th48;

consider k being Nat such that

A4: k > 0 and

A5: a in C |^ k by A1, Th48;

a ^ b in C |^ (k + l) by A5, A3, FLANG_1:40;

hence a ^ b in C + by A4, Th48; :: thesis: verum