let E be set ; :: thesis: for C being Subset of (E ^omega)

for a, b being Element of E ^omega

for m, n being Nat st a in C |^.. m & b in C |^.. n holds

a ^ b in C |^.. (m + n)

let C be Subset of (E ^omega); :: thesis: for a, b being Element of E ^omega

for m, n being Nat st a in C |^.. m & b in C |^.. n holds

a ^ b in C |^.. (m + n)

let a, b be Element of E ^omega ; :: thesis: for m, n being Nat st a in C |^.. m & b in C |^.. n holds

a ^ b in C |^.. (m + n)

let m, n be Nat; :: thesis: ( a in C |^.. m & b in C |^.. n implies a ^ b in C |^.. (m + n) )

assume that

A1: a in C |^.. m and

A2: b in C |^.. n ; :: thesis: a ^ b in C |^.. (m + n)

A3: (C |^.. m) ^^ (C |^.. n) c= C |^.. (m + n) by Th21;

a ^ b in (C |^.. m) ^^ (C |^.. n) by A1, A2, FLANG_1:def 1;

hence a ^ b in C |^.. (m + n) by A3; :: thesis: verum

for a, b being Element of E ^omega

for m, n being Nat st a in C |^.. m & b in C |^.. n holds

a ^ b in C |^.. (m + n)

let C be Subset of (E ^omega); :: thesis: for a, b being Element of E ^omega

for m, n being Nat st a in C |^.. m & b in C |^.. n holds

a ^ b in C |^.. (m + n)

let a, b be Element of E ^omega ; :: thesis: for m, n being Nat st a in C |^.. m & b in C |^.. n holds

a ^ b in C |^.. (m + n)

let m, n be Nat; :: thesis: ( a in C |^.. m & b in C |^.. n implies a ^ b in C |^.. (m + n) )

assume that

A1: a in C |^.. m and

A2: b in C |^.. n ; :: thesis: a ^ b in C |^.. (m + n)

A3: (C |^.. m) ^^ (C |^.. n) c= C |^.. (m + n) by Th21;

a ^ b in (C |^.. m) ^^ (C |^.. n) by A1, A2, FLANG_1:def 1;

hence a ^ b in C |^.. (m + n) by A3; :: thesis: verum