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