let E be set ; :: thesis: for C being Subset of (E ^omega)
for a, b being Element of E ^omega
for n, m 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 n, m 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 n, m being Nat st a in C |^ m & b in C |^ n holds
a ^ b in C |^ (m + n)
let n, m be Nat; :: thesis: ( a in C |^ m & b in C |^ n implies a ^ b in C |^ (m + n) )
assume ( a in C |^ m & b in C |^ n ) ; :: thesis: a ^ b in C |^ (m + n)
then a ^ b in (C |^ m) ^^ (C |^ n) by Def1;
hence a ^ b in C |^ (m + n) by Th33; :: thesis: verum