let V be non empty set ; :: thesis: Maps V = union { (Maps A,B) where A, B is Element of V : verum }
set M = { (Maps A,B) where A, B is Element of V : verum } ;

now

let z be set ; :: thesis: ( ( z in Maps V implies z in union { (Maps A,B) where A, B is Element of V : verum } ) & ( z in union { (Maps A,B) where A, B is Element of V : verum } implies z in Maps V ) )
thus ( z in Maps V implies z in union { (Maps A,B) where A, B is Element of V : verum } ) :: thesis: ( z in union { (Maps A,B) where A, B is Element of V : verum } implies z in Maps V )

proof

assume z in Maps V ; :: thesis: z in union { (Maps A,B) where A, B is Element of V : verum }
then consider f being Element of Funcs V, A, B being Element of V such that
A1: ( z = [[A,B],f] & ( B = {} implies A = {} ) & f is Function of A,B ) by Th4;
( z in Maps A,B & Maps A,B in { (Maps A,B) where A, B is Element of V : verum } ) by A1, Th15;
hence z in union { (Maps A,B) where A, B is Element of V : verum } by TARSKI:def 4; :: thesis: verum

end;

assume z in union { (Maps A,B) where A, B is Element of V : verum } ; :: thesis: z in Maps V
then consider C being set such that
A2: z in C and
A3: C in { (Maps A,B) where A, B is Element of V : verum } by TARSKI:def 4;
consider A, B being Element of V such that
A4: C = Maps A,B by A3;
ex f being Element of Funcs V st
( z = [[A,B],f] & [[A,B],f] in Maps V ) by A2, A4;
hence z in Maps V ; :: thesis: verum

end;

hence Maps V = union { (Maps A,B) where A, B is Element of V : verum } by TARSKI:2; :: thesis: verum