let s, t be Tree; :: thesis: Leaves (tree (t,s)) = { (<*0*> ^ p) where p is Element of t : p in Leaves t } \/ { (<*1*> ^ p) where p is Element of s : p in Leaves s }
set L = { (<*0*> ^ p) where p is Element of t : p in Leaves t } ;
set R = { (<*1*> ^ p) where p is Element of s : p in Leaves s } ;
set H = Leaves (tree (t,s));
set q = <*t,s*>;
A1: len <*t,s*> = 2 by FINSEQ_1:44;
A2: <*t,s*> . 1 = t by FINSEQ_1:44;
A3: <*t,s*> . 2 = s by FINSEQ_1:44;
for x being object holds
( x in Leaves (tree (t,s)) iff x in { (<*0*> ^ p) where p is Element of t : p in Leaves t } \/ { (<*1*> ^ p) where p is Element of s : p in Leaves s } )
proof
let x be object ; :: thesis: ( x in Leaves (tree (t,s)) iff x in { (<*0*> ^ p) where p is Element of t : p in Leaves t } \/ { (<*1*> ^ p) where p is Element of s : p in Leaves s } )
hereby :: thesis: ( x in { (<*0*> ^ p) where p is Element of t : p in Leaves t } \/ { (<*1*> ^ p) where p is Element of s : p in Leaves s } implies x in Leaves (tree (t,s)) )
assume A4: x in Leaves (tree (t,s)) ; :: thesis: x in { (<*0*> ^ p) where p is Element of t : p in Leaves t } \/ { (<*1*> ^ p) where p is Element of s : p in Leaves s }
then ( x = {} or ex n being Nat ex r being FinSequence st
( n < len <*t,s*> & r in <*t,s*> . (n + 1) & x = <*n*> ^ r ) ) by TREES_3:def 15;
then consider n being Nat, r being FinSequence such that
A5: ( n < len <*t,s*> & r in <*t,s*> . (n + 1) & x = <*n*> ^ r ) by A4, Th9;
per cases ( n = 0 or n = 1 ) by NAT_1:23, A1, A5;
suppose A6: n = 0 ; :: thesis: x in { (<*0*> ^ p) where p is Element of t : p in Leaves t } \/ { (<*1*> ^ p) where p is Element of s : p in Leaves s }
then r in Leaves t by BINTREE1:6, A4, A2, A5;
then x in { (<*0*> ^ p) where p is Element of t : p in Leaves t } by A6, A5;
hence x in { (<*0*> ^ p) where p is Element of t : p in Leaves t } \/ { (<*1*> ^ p) where p is Element of s : p in Leaves s } by XBOOLE_0:def 3; :: thesis: verum
end;
suppose A7: n = 1 ; :: thesis: x in { (<*0*> ^ p) where p is Element of t : p in Leaves t } \/ { (<*1*> ^ p) where p is Element of s : p in Leaves s }
then r in Leaves s by BINTREE1:6, A4, A5, A3;
then x in { (<*1*> ^ p) where p is Element of s : p in Leaves s } by A7, A5;
hence x in { (<*0*> ^ p) where p is Element of t : p in Leaves t } \/ { (<*1*> ^ p) where p is Element of s : p in Leaves s } by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
assume A8: x in { (<*0*> ^ p) where p is Element of t : p in Leaves t } \/ { (<*1*> ^ p) where p is Element of s : p in Leaves s } ; :: thesis: x in Leaves (tree (t,s))
per cases ( x in { (<*0*> ^ p) where p is Element of t : p in Leaves t } or x in { (<*1*> ^ p) where p is Element of s : p in Leaves s } ) by A8, XBOOLE_0:def 3;
suppose x in { (<*0*> ^ p) where p is Element of t : p in Leaves t } ; :: thesis: x in Leaves (tree (t,s))
then consider p being Element of t such that
A9: ( x = <*0*> ^ p & p in Leaves t ) ;
( 0 < len <*t,s*> & p in <*t,s*> . (0 + 1) ) by A2;
then x in tree (t,s) by A9, TREES_3:def 15;
hence x in Leaves (tree (t,s)) by BINTREE1:6, A9; :: thesis: verum
end;
suppose x in { (<*1*> ^ p) where p is Element of s : p in Leaves s } ; :: thesis: x in Leaves (tree (t,s))
then consider p being Element of s such that
A10: ( x = <*1*> ^ p & p in Leaves s ) ;
( 1 < len <*t,s*> & p in <*t,s*> . (1 + 1) ) by A1, A3;
then x in tree (t,s) by A10, TREES_3:def 15;
hence x in Leaves (tree (t,s)) by BINTREE1:6, A10; :: thesis: verum
end;
end;
end;
hence Leaves (tree (t,s)) = { (<*0*> ^ p) where p is Element of t : p in Leaves t } \/ { (<*1*> ^ p) where p is Element of s : p in Leaves s } by TARSKI:2; :: thesis: verum