let S be ManySortedSign ; :: thesis: for o being set
for t1, t2 being DecoratedTree holds S variables_in ([o, the carrier of S] -tree <*t1,t2*>) = (S variables_in t1) (\/) (S variables_in t2)
let o be set ; :: thesis: for t1, t2 being DecoratedTree holds S variables_in ([o, the carrier of S] -tree <*t1,t2*>) = (S variables_in t1) (\/) (S variables_in t2)
let t1, t2 be DecoratedTree; :: thesis: S variables_in ([o, the carrier of S] -tree <*t1,t2*>) = (S variables_in t1) (\/) (S variables_in t2)
now :: thesis: for s being object st s in the carrier of S holds
(S variables_in ([o, the carrier of S] -tree <*t1,t2*>)) . s = ((S variables_in t1) (\/) (S variables_in t2)) . s
let s be object ; :: thesis: ( s in the carrier of S implies (S variables_in ([o, the carrier of S] -tree <*t1,t2*>)) . s = ((S variables_in t1) (\/) (S variables_in t2)) . s )
assume A1: s in the carrier of S ; :: thesis: (S variables_in ([o, the carrier of S] -tree <*t1,t2*>)) . s = ((S variables_in t1) (\/) (S variables_in t2)) . s
A2: t1 in {t1,t2} by TARSKI:def 2;
A3: t2 in {t1,t2} by TARSKI:def 2;
now :: thesis: for x being object holds
( x in (S variables_in ([o, the carrier of S] -tree <*t1,t2*>)) . s iff x in ((S variables_in t1) (\/) (S variables_in t2)) . s )
let x be object ; :: thesis: ( x in (S variables_in ([o, the carrier of S] -tree <*t1,t2*>)) . s iff x in ((S variables_in t1) (\/) (S variables_in t2)) . s )
rng <*t1,t2*> = {t1,t2} by FINSEQ_2:127;
then ( x in (S variables_in ([o, the carrier of S] -tree <*t1,t2*>)) . s iff ex q being DecoratedTree st
( q in {t1,t2} & x in (S variables_in q) . s ) ) by A1, MSAFREE3:11;
then ( x in (S variables_in ([o, the carrier of S] -tree <*t1,t2*>)) . s iff ( x in (S variables_in t1) . s or x in (S variables_in t2) . s ) ) by A2, A3, TARSKI:def 2;
then ( x in (S variables_in ([o, the carrier of S] -tree <*t1,t2*>)) . s iff x in ((S variables_in t1) . s) \/ ((S variables_in t2) . s) ) by XBOOLE_0:def 3;
hence ( x in (S variables_in ([o, the carrier of S] -tree <*t1,t2*>)) . s iff x in ((S variables_in t1) (\/) (S variables_in t2)) . s ) by A1, PBOOLE:def 4; :: thesis: verum
end;
hence (S variables_in ([o, the carrier of S] -tree <*t1,t2*>)) . s = ((S variables_in t1) (\/) (S variables_in t2)) . s by TARSKI:2; :: thesis: verum
end;
hence S variables_in ([o, the carrier of S] -tree <*t1,t2*>) = (S variables_in t1) (\/) (S variables_in t2) ; :: thesis: verum