let E be set ; 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); 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 ; ( a in C + & b in C + implies a ^ b in C + )
assume that
A1:
a in C +
and
A2:
b in C +
; 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; verum