take F = [#] ( the Sorts of L . the formula-sort of S); :: thesis: F is V AL-closed

let A be Formula of L; :: according to AOFA_L00:def 47 :: thesis: for B being Formula of L holds

( ( for M being Algorithm of L holds

( (M * (A \and B)) \iff ((M * A) \and (M * B)) in F & (M * (A \or B)) \iff ((M * A) \or (M * B)) in F & (\Cup (M,A)) \iff (A \or (\Cup (M,(M * A)))) in F & (\Cap (M,A)) \iff (A \and (\Cap (M,(M * A)))) in F & ( A \imp B in F implies ( (\Cup (M,A)) \imp (\Cup (M,B)) in F & (\Cap (M,A)) \imp (\Cap (M,B)) in F ) ) ) ) & ( for a being SortSymbol of J

for x being Element of X . a

for x0 being Element of Union (X extended_by ({}, the carrier of S)) st x = x0 holds

for t being Element of the Sorts of T . a

for t1 being Element of Union the Sorts of L st t1 = t holds

( ((x := (t,L)) * A) \iff (A / (x0,t1)) in F & ( for y being Element of X . a st y nin (vf t) . a holds

for y0 being Element of Union (X extended_by ({}, the carrier of S)) st y = y0 holds

((x := (t,L)) * (\ex (x,A))) \iff (\ex (y,((x := (t,L)) * ((y := ((@ x),L)) * (A / (x0,y0)))))) in F ) & ((x := (t,L)) * A) \imp (\ex (x,A)) in F ) ) & ( for M, M1, M2 being Algorithm of L holds

( ((M \; M1) * A) \iff (M * (M1 * A)) in F & ((if-then-else (M,M1,M2)) * A) \iff (((M * V) \and (M * (M1 * A))) \or ((M * (\not V)) \and (M * (M2 * A)))) in F & ((while (M,M1)) * A) \iff (((M * (\not V)) \and A) \or ((M * V) \and (M * (M1 * ((while (M,M1)) * A))))) in F ) ) )

F = the Sorts of L . the formula-sort of S by SUBSET_1:def 3;

hence for B being Formula of L holds

( ( for M being Algorithm of L holds

( (M * (A \and B)) \iff ((M * A) \and (M * B)) in F & (M * (A \or B)) \iff ((M * A) \or (M * B)) in F & (\Cup (M,A)) \iff (A \or (\Cup (M,(M * A)))) in F & (\Cap (M,A)) \iff (A \and (\Cap (M,(M * A)))) in F & ( A \imp B in F implies ( (\Cup (M,A)) \imp (\Cup (M,B)) in F & (\Cap (M,A)) \imp (\Cap (M,B)) in F ) ) ) ) & ( for a being SortSymbol of J

for x being Element of X . a

for x0 being Element of Union (X extended_by ({}, the carrier of S)) st x = x0 holds

for t being Element of the Sorts of T . a

for t1 being Element of Union the Sorts of L st t1 = t holds

( ((x := (t,L)) * A) \iff (A / (x0,t1)) in F & ( for y being Element of X . a st y nin (vf t) . a holds

for y0 being Element of Union (X extended_by ({}, the carrier of S)) st y = y0 holds

((x := (t,L)) * (\ex (x,A))) \iff (\ex (y,((x := (t,L)) * ((y := ((@ x),L)) * (A / (x0,y0)))))) in F ) & ((x := (t,L)) * A) \imp (\ex (x,A)) in F ) ) & ( for M, M1, M2 being Algorithm of L holds

( ((M \; M1) * A) \iff (M * (M1 * A)) in F & ((if-then-else (M,M1,M2)) * A) \iff (((M * V) \and (M * (M1 * A))) \or ((M * (\not V)) \and (M * (M2 * A)))) in F & ((while (M,M1)) * A) \iff (((M * (\not V)) \and A) \or ((M * V) \and (M * (M1 * ((while (M,M1)) * A))))) in F ) ) ) ; :: thesis: verum

let A be Formula of L; :: according to AOFA_L00:def 47 :: thesis: for B being Formula of L holds

( ( for M being Algorithm of L holds

( (M * (A \and B)) \iff ((M * A) \and (M * B)) in F & (M * (A \or B)) \iff ((M * A) \or (M * B)) in F & (\Cup (M,A)) \iff (A \or (\Cup (M,(M * A)))) in F & (\Cap (M,A)) \iff (A \and (\Cap (M,(M * A)))) in F & ( A \imp B in F implies ( (\Cup (M,A)) \imp (\Cup (M,B)) in F & (\Cap (M,A)) \imp (\Cap (M,B)) in F ) ) ) ) & ( for a being SortSymbol of J

for x being Element of X . a

for x0 being Element of Union (X extended_by ({}, the carrier of S)) st x = x0 holds

for t being Element of the Sorts of T . a

for t1 being Element of Union the Sorts of L st t1 = t holds

( ((x := (t,L)) * A) \iff (A / (x0,t1)) in F & ( for y being Element of X . a st y nin (vf t) . a holds

for y0 being Element of Union (X extended_by ({}, the carrier of S)) st y = y0 holds

((x := (t,L)) * (\ex (x,A))) \iff (\ex (y,((x := (t,L)) * ((y := ((@ x),L)) * (A / (x0,y0)))))) in F ) & ((x := (t,L)) * A) \imp (\ex (x,A)) in F ) ) & ( for M, M1, M2 being Algorithm of L holds

( ((M \; M1) * A) \iff (M * (M1 * A)) in F & ((if-then-else (M,M1,M2)) * A) \iff (((M * V) \and (M * (M1 * A))) \or ((M * (\not V)) \and (M * (M2 * A)))) in F & ((while (M,M1)) * A) \iff (((M * (\not V)) \and A) \or ((M * V) \and (M * (M1 * ((while (M,M1)) * A))))) in F ) ) )

F = the Sorts of L . the formula-sort of S by SUBSET_1:def 3;

hence for B being Formula of L holds

( ( for M being Algorithm of L holds

( (M * (A \and B)) \iff ((M * A) \and (M * B)) in F & (M * (A \or B)) \iff ((M * A) \or (M * B)) in F & (\Cup (M,A)) \iff (A \or (\Cup (M,(M * A)))) in F & (\Cap (M,A)) \iff (A \and (\Cap (M,(M * A)))) in F & ( A \imp B in F implies ( (\Cup (M,A)) \imp (\Cup (M,B)) in F & (\Cap (M,A)) \imp (\Cap (M,B)) in F ) ) ) ) & ( for a being SortSymbol of J

for x being Element of X . a

for x0 being Element of Union (X extended_by ({}, the carrier of S)) st x = x0 holds

for t being Element of the Sorts of T . a

for t1 being Element of Union the Sorts of L st t1 = t holds

( ((x := (t,L)) * A) \iff (A / (x0,t1)) in F & ( for y being Element of X . a st y nin (vf t) . a holds

for y0 being Element of Union (X extended_by ({}, the carrier of S)) st y = y0 holds

((x := (t,L)) * (\ex (x,A))) \iff (\ex (y,((x := (t,L)) * ((y := ((@ x),L)) * (A / (x0,y0)))))) in F ) & ((x := (t,L)) * A) \imp (\ex (x,A)) in F ) ) & ( for M, M1, M2 being Algorithm of L holds

( ((M \; M1) * A) \iff (M * (M1 * A)) in F & ((if-then-else (M,M1,M2)) * A) \iff (((M * V) \and (M * (M1 * A))) \or ((M * (\not V)) \and (M * (M2 * A)))) in F & ((while (M,M1)) * A) \iff (((M * (\not V)) \and A) \or ((M * V) \and (M * (M1 * ((while (M,M1)) * A))))) in F ) ) ) ; :: thesis: verum