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 :: thesis: for z being object holds
( ( 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 ) )

let z be object ; :: 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;
A2: Maps (A,B) in { (Maps (A,B)) where A, B is Element of V : verum } ;
z in Maps (A,B) by A1, Th15;
hence z in union { (Maps (A,B)) where A, B is Element of V : verum } by A2, 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
A3: z in C and
A4: 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
A5: C = Maps (A,B) by A4;
ex f being Element of Funcs V st
( z = [[A,B],f] & [[A,B],f] in Maps V ) by A3, A5;
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