union { (x . O) where x is Element of X : x in L } = | L

proof

thus union { (x . O) where x is Element of X : x in L } c= | L :: according to XBOOLE_0:def 10 :: thesis: | L c= union { (x . O) where x is Element of X : x in L }

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in union { (x . O) where x is Element of X : x in L } or z in | L )
assume z in union { (x . O) where x is Element of X : x in L } ; :: thesis: z in | L
then consider Y being set such that
A1: ( z in Y & Y in { (x . O) where x is Element of X : x in L } ) by TARSKI:def 4;
consider x being Element of X such that
A2: ( Y = x . O & x in L ) by A1;
[x,z] in O by A1, A2, RELAT_1:169;
hence z in | L by A2, RELAT_1:def 13; :: thesis: verum

end;

thus | L c= union { (x . O) where x is Element of X : x in L } :: thesis: verum

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in | L or z in union { (x . O) where x is Element of X : x in L } )
assume z in | L ; :: thesis: z in union { (x . O) where x is Element of X : x in L }
then consider y being object such that
A3: ( [y,z] in O & y in L ) by RELAT_1:def 13;
reconsider y = y as Element of X by A3;
( z in y . O & y . O in { (x . O) where x is Element of X : x in L } ) by A3, RELAT_1:169;
hence z in union { (x . O) where x is Element of X : x in L } by TARSKI:def 4; :: thesis: verum

end;

end;

hence for b₁ being List of X holds
( b₁ = | L iff b₁ = union { (x . O) where x is Element of X : x in L } ) ; :: thesis: verum