let t be Tree; :: thesis: for p, q being FinSequence of NAT st p ^ q in t holds
t | (p ^ q) = (t | p) | q
let p, q be FinSequence of NAT ; :: thesis: ( p ^ q in t implies t | (p ^ q) = (t | p) | q )
assume A1: p ^ q in t ; :: thesis: t | (p ^ q) = (t | p) | q
then A2: p in t by TREES_1:46;
then A3: q in t | p by A1, TREES_1:def 9;
let r be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not r in t | (p ^ q) or r in (t | p) | q ) & ( not r in (t | p) | q or r in t | (p ^ q) ) )
(p ^ q) ^ r = p ^ (q ^ r) by FINSEQ_1:45;
then ( ( r in t | (p ^ q) implies (p ^ q) ^ r in t ) & ( (p ^ q) ^ r in t implies r in t | (p ^ q) ) & ( r in (t | p) | q implies q ^ r in t | p ) & ( q ^ r in t | p implies r in (t | p) | q ) & ( q ^ r in t | p implies (p ^ q) ^ r in t ) & ( (p ^ q) ^ r in t implies q ^ r in t | p ) ) by A1, A2, A3, TREES_1:def 9;
hence ( ( not r in t | (p ^ q) or r in (t | p) | q ) & ( not r in (t | p) | q or r in t | (p ^ q) ) ) ; :: thesis: verum