let A be preIfWhileAlgebra; 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; 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 ; 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; 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; ( 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
; 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; ( f . (s,C) nin T implies f . (s,(if-then (C,I))) = f . (s,C) )
assume
f . (s,C) nin T
; 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
;
verum