let A be preIfWhileAlgebra; :: thesis: for S being non empty set
for T being Subset of S
for f being ExecutionFunction of A,S,T
for P being set
for I, J being Element of A st P is_invariant_wrt I,f & P is_invariant_wrt J,f holds
P is_invariant_wrt I \; J,f
let S be non empty set ; :: thesis: for T being Subset of S
for f being ExecutionFunction of A,S,T
for P being set
for I, J being Element of A st P is_invariant_wrt I,f & P is_invariant_wrt J,f holds
P is_invariant_wrt I \; J,f
let T be Subset of S; :: thesis: for f being ExecutionFunction of A,S,T
for P being set
for I, J being Element of A st P is_invariant_wrt I,f & P is_invariant_wrt J,f holds
P is_invariant_wrt I \; J,f
let f be ExecutionFunction of A,S,T; :: thesis: for P being set
for I, J being Element of A st P is_invariant_wrt I,f & P is_invariant_wrt J,f holds
P is_invariant_wrt I \; J,f
let P be set ; :: thesis: for I, J being Element of A st P is_invariant_wrt I,f & P is_invariant_wrt J,f holds
P is_invariant_wrt I \; J,f
let I, J be Element of A; :: thesis: ( P is_invariant_wrt I,f & P is_invariant_wrt J,f implies P is_invariant_wrt I \; J,f )
assume that
A1: for s being Element of S st s in P holds
f . (s,I) in P and
A2: for s being Element of S st s in P holds
f . (s,J) in P ; :: according to AOFA_000:def 39 :: thesis: P is_invariant_wrt I \; J,f
let s be Element of S; :: according to AOFA_000:def 39 :: thesis: ( s in P implies f . (s,(I \; J)) in P )
assume s in P ; :: thesis: f . (s,(I \; J)) in P
then A3: f . (s,I) in P by A1;
f . (s,(I \; J)) = f . ((f . (s,I)),J) by Def29;
hence f . (s,(I \; J)) in P by A2, A3; :: thesis: verum