let A be preIfWhileAlgebra; :: thesis: for C, I being Element of A
for S being non empty set
for T being Subset of S
for f being Function of [:S,the carrier of A:],S st f is complying_with_empty-instruction & f complies_with_if_wrt T holds
for s being Element of S st f . s,C nin T holds
f . s,(if-then C,I) = f . s,C
let C, I be Element of A; :: thesis: for S being non empty set
for T being Subset of S
for f being Function of [:S,the carrier of A:],S st f is complying_with_empty-instruction & f complies_with_if_wrt T holds
for s being Element of S st f . s,C nin T holds
f . s,(if-then C,I) = f . s,C
let S be non empty set ; :: thesis: for T being Subset of S
for f being Function of [:S,the carrier of A:],S st f is complying_with_empty-instruction & f complies_with_if_wrt T holds
for s being Element of S st f . s,C nin T holds
f . s,(if-then C,I) = f . s,C
let T be Subset of S; :: thesis: for f being Function of [:S,the carrier of A:],S st f is complying_with_empty-instruction & f complies_with_if_wrt T holds
for s being Element of S st f . s,C nin T holds
f . s,(if-then C,I) = f . s,C
let f be Function of [:S,the carrier of A:],S; :: thesis: ( f is complying_with_empty-instruction & f complies_with_if_wrt T implies for s being Element of S st f . s,C nin T holds
f . s,(if-then C,I) = f . s,C )
assume that
A1: f is complying_with_empty-instruction and
A2: f complies_with_if_wrt T ; :: thesis: for s being Element of S st f . s,C nin T holds
f . s,(if-then C,I) = f . s,C
let s be Element of S; :: thesis: ( f . s,C nin T implies f . s,(if-then C,I) = f . s,C )
assume f . s,C nin T ; :: thesis: f . s,(if-then C,I) = f . s,C
hence f . s,(if-then C,I) = f . (f . s,C),(EmptyIns A) by Def30, A2
.= f . s,C by Def28, A1 ;
:: thesis: verum