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 ( 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 Th34; :: thesis: verum