set f = the Function of VAR,E;

take F = def_func' (H, the Function of VAR,E); :: thesis: for g being Function of VAR,E holds

( E,g |= H iff F . (g . (x. 3)) = g . (x. 4) )

let g be Function of VAR,E; :: thesis: ( E,g |= H iff F . (g . (x. 3)) = g . (x. 4) )

set j = the Function of VAR,E +* ((x. 3),(g . (x. 3)));

set h = ( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)));

thus ( E,g |= H implies F . (g . (x. 3)) = g . (x. 4) ) :: thesis: ( F . (g . (x. 3)) = g . (x. 4) implies E,g |= H )

A14: F . (g . (x. 3)) = g . (x. 4) and

A15: not E,g |= H ; :: thesis: contradiction

A16: ( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) . (x. 3) = g . (x. 3) by FUNCT_7:128;

then ( (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . (x. 4) = g . (x. 4) & F . ((( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . (x. 3)) <> (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . (x. 4) ) by A7, A3, Def1, FUNCT_7:128;

hence contradiction by A14, A16, FUNCT_7:32; :: thesis: verum

take F = def_func' (H, the Function of VAR,E); :: thesis: for g being Function of VAR,E holds

( E,g |= H iff F . (g . (x. 3)) = g . (x. 4) )

let g be Function of VAR,E; :: thesis: ( E,g |= H iff F . (g . (x. 3)) = g . (x. 4) )

set j = the Function of VAR,E +* ((x. 3),(g . (x. 3)));

set h = ( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)));

A3: now :: thesis: for x being Variable st (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x <> the Function of VAR,E . x & x. 0 <> x & x. 3 <> x holds

not x. 4 <> x

A7:
( not x. 0 in Free H & E, the Function of VAR,E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) )
by A1, A2, TARSKI:def 2;not x. 4 <> x

let x be Variable; :: thesis: ( (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x <> the Function of VAR,E . x & x. 0 <> x & x. 3 <> x implies not x. 4 <> x )

assume that

A4: (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x <> the Function of VAR,E . x and

x. 0 <> x and

A5: x. 3 <> x and

A6: x. 4 <> x ; :: thesis: contradiction

(( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x = ( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) . x by A6, FUNCT_7:32

.= the Function of VAR,E . x by A5, FUNCT_7:32 ;

hence contradiction by A4; :: thesis: verum

end;assume that

A4: (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x <> the Function of VAR,E . x and

x. 0 <> x and

A5: x. 3 <> x and

A6: x. 4 <> x ; :: thesis: contradiction

(( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x = ( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) . x by A6, FUNCT_7:32

.= the Function of VAR,E . x by A5, FUNCT_7:32 ;

hence contradiction by A4; :: thesis: verum

thus ( E,g |= H implies F . (g . (x. 3)) = g . (x. 4) ) :: thesis: ( F . (g . (x. 3)) = g . (x. 4) implies E,g |= H )

proof

assume that
set g3 = the Function of VAR,E +* ((x. 3),(g . (x. 3)));

set g4 = ( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)));

then E,( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4))) |= H by A13, Th13;

then ( (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . (x. 4) = g . (x. 4) & F . ((( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . (x. 3)) = (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . (x. 4) ) by A7, A8, Def1, FUNCT_7:128;

hence F . (g . (x. 3)) = g . (x. 4) by A12, FUNCT_7:32; :: thesis: verum

end;set g4 = ( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)));

A8: now :: thesis: for x being Variable st (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x <> the Function of VAR,E . x & x. 0 <> x & x. 3 <> x holds

not x. 4 <> x

A12:
( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) . (x. 3) = g . (x. 3)
by FUNCT_7:128;not x. 4 <> x

let x be Variable; :: thesis: ( (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x <> the Function of VAR,E . x & x. 0 <> x & x. 3 <> x implies not x. 4 <> x )

assume that

A9: (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x <> the Function of VAR,E . x and

x. 0 <> x and

A10: x. 3 <> x and

A11: x. 4 <> x ; :: thesis: contradiction

(( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x = ( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) . x by A11, FUNCT_7:32

.= the Function of VAR,E . x by A10, FUNCT_7:32 ;

hence contradiction by A9; :: thesis: verum

end;assume that

A9: (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x <> the Function of VAR,E . x and

x. 0 <> x and

A10: x. 3 <> x and

A11: x. 4 <> x ; :: thesis: contradiction

(( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x = ( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) . x by A11, FUNCT_7:32

.= the Function of VAR,E . x by A10, FUNCT_7:32 ;

hence contradiction by A9; :: thesis: verum

A13: now :: thesis: for x being Variable st g . x <> (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x holds

not x in Free H

assume
E,g |= H
; :: thesis: F . (g . (x. 3)) = g . (x. 4)not x in Free H

let x be Variable; :: thesis: ( g . x <> (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x implies not x in Free H )

assume g . x <> (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x ; :: thesis: not x in Free H

then ( x. 4 <> x & x. 3 <> x ) by A12, FUNCT_7:32, FUNCT_7:128;

hence not x in Free H by A1, TARSKI:def 2; :: thesis: verum

end;assume g . x <> (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x ; :: thesis: not x in Free H

then ( x. 4 <> x & x. 3 <> x ) by A12, FUNCT_7:32, FUNCT_7:128;

hence not x in Free H by A1, TARSKI:def 2; :: thesis: verum

then E,( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4))) |= H by A13, Th13;

then ( (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . (x. 4) = g . (x. 4) & F . ((( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . (x. 3)) = (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . (x. 4) ) by A7, A8, Def1, FUNCT_7:128;

hence F . (g . (x. 3)) = g . (x. 4) by A12, FUNCT_7:32; :: thesis: verum

A14: F . (g . (x. 3)) = g . (x. 4) and

A15: not E,g |= H ; :: thesis: contradiction

A16: ( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) . (x. 3) = g . (x. 3) by FUNCT_7:128;

now :: thesis: for x being Variable st (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x <> g . x holds

not x in Free H

then
not E,( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4))) |= H
by A15, Th13;not x in Free H

let x be Variable; :: thesis: ( (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x <> g . x implies not x in Free H )

assume (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x <> g . x ; :: thesis: not x in Free H

then ( x. 4 <> x & x. 3 <> x ) by A16, FUNCT_7:32, FUNCT_7:128;

hence not x in Free H by A1, TARSKI:def 2; :: thesis: verum

end;assume (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x <> g . x ; :: thesis: not x in Free H

then ( x. 4 <> x & x. 3 <> x ) by A16, FUNCT_7:32, FUNCT_7:128;

hence not x in Free H by A1, TARSKI:def 2; :: thesis: verum

then ( (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . (x. 4) = g . (x. 4) & F . ((( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . (x. 3)) <> (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . (x. 4) ) by A7, A3, Def1, FUNCT_7:128;

hence contradiction by A14, A16, FUNCT_7:32; :: thesis: verum