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 } ;

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 ) )

hence
Maps V = union { (Maps (A,B)) where A, B is Element of V : verum }
by TARSKI:2; :: thesis: verum( ( 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 )

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;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 union { (Maps (A,B)) where A, B is Element of V : verum }
; :: thesis: z in Maps V
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;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

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