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 A2
.= f . (s,C) by A1 ;
:: thesis: verum